> > Juan wrote: > A trivial example of Hott with Lean... In my case, I learned UniMath just from Voevodsky's video lectures at Oxford (I was not there): Point 9 in this link: https://www.math.ias.edu/vladimir/Lectures I am interested to get back to HoTT, after some time focused in Isabelle/HOL, just for pleasure (my serious job is with Isabelle/HOL). What I love of HoTT is the idea of thinking in a topological way about non-topological problems: this is like a video-game for me, not a project, it is something just for fun. Here is an example of one of my theorems in UniMath (a greedy generalization of Euclidean division). As you can see, automation is almost zero in my program. I guess that it will be shorted in Lean or in Coq (using the HoTT library). [Another motivation is that I have the intuition that HoTT is related to the combinatorics of finite fields via the Weil Conjectures, but I need more experience before to formalize this intuition, e.g., given a type, we can express its topological invariants as the number of points on a variety over a finite field and the correspondence is "natural". This may be non-sense.] Unset Automatic Introduction. (** *** Imports *) Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Foundations.PartA. Definition Increasing := fun (f : nat -> nat) => forall n : nat, f n ≤ f (S n). Lemma powerMonotonic : forall f : nat -> nat, Increasing f -> ( forall n k : nat, f n ≤ f (n + k) ). Proof. intros. intros. induction k. rewrite natplusr0. apply (natlehmplusnm 0 (f n) ). change (S k) with (1 + k). rewrite (natpluscomm 1 k). rewrite <- (natplusassoc n k 1). unfold Increasing in X. specialize (X (n + k)). change (S (n + k)) with (1 + (n + k)) in X. rewrite ( natpluscomm 1 (n + k) ) in X. apply (istransnatleh IHk X). Defined. Definition SIncreasing := fun (f : nat -> nat) => forall n : nat, f n < f (S n). Lemma SpowerMonotonic : forall f : nat -> nat, SIncreasing f -> ( forall n k : nat, f n < f (n + k + 1) ). Proof. intros. intros. induction k. rewrite natplusr0. rewrite -> (natpluscomm n 1). change (1 + n) with (S n). unfold SIncreasing in X. specialize (X n). apply X. change (S k) with (1 + k). rewrite (natpluscomm 1 k). rewrite <- (natplusassoc n k 1). unfold SIncreasing in X. specialize (X (n + k + 1)). rewrite -> (natpluscomm (n + k) 1) in X. change (S (1 + (n + k))) with (1 + (1 + (n + k))) in X. rewrite <-( natplusassoc 1 1 (n + k) ) in X. rewrite -> ( natpluscomm (1 + 1) (n + k) ) in X. rewrite -> ( natplusassoc n k (1 + 1) ) in X. rewrite -> ( natplusassoc (n + k) 1 1 ). rewrite -> ( natpluscomm (n + k) 1 ) in IHk. assert (T := istransnatlth (f n) (f (1 + (n + k))) (f (n + (k + (1 + 1)))) ). rewrite -> ( natplusassoc n k (1 + 1) ). apply T. apply IHk. apply X. Defined. Lemma SpowerLargerThanN : forall f : nat -> nat, SIncreasing f -> ( forall n : nat, (f 0) + n ≤ f n ). Proof. induction n. rewrite (natplusr0 (f 0)). apply (natlehmplusnm 0). rewrite <- ( plus_n_Sm (f 0) n). apply (natlehandplusl (f 0 + n) (f n) 1 ) in IHn. change (1 + (f 0 + n)) with (S (f 0 + n)) in IHn. change (1 + f n) with (S (f n)) in IHn. unfold SIncreasing in X. specialize (X n). apply (natlthtolehsn) in X. apply ( istransnatleh IHn X ). Defined. Definition EuclidF := fun (f : nat -> nat) (x : dirprod nat nat) => (f (pr1 x)) + (pr2 x). Definition GreedyEuclid (f : nat -> nat) (isSIncreasing : SIncreasing f) (n : nat) : dirprod nat nat. Proof. intros. induction n as [ | n x]. - intros. apply (dirprodpair (f 0) 0). - induction (natlthorgeh ((f (pr1 x)) + S (pr2 x)) (f (S (pr1 x)))). + apply ( dirprodpair (pr1 x) (S (pr2 x)) ). + apply ( dirprodpair (S (pr1 x)) (0) ). Defined. Lemma GreedyEuclidLem : forall (f : nat -> nat), SIncreasing f -> forall n : nat, hfiber (fun (x : dirprod nat nat) => EuclidF f x) ((f 0) + n). Proof. intros. unfold hfiber. exists (dirprodpair 0 n). unfold EuclidF. simpl. apply idpath. Defined. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout.