Re: [HoTT] The best proof assistant for HoTT from the point of view of automation

["José Manuel Rodriguez Caballero" <josephcmac@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 4488 bytes --]

>
> 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.

[-- Attachment #2: Type: text/html, Size: 6178 bytes --]