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.