comment examples

Author: tabareau

Prime.v

@@ -13,6 +13,10 @@ Notation " ( x ; p ) " := (sigmaPI _ x p).
 Inductive sFalse : SProp := .
 Inductive sTrue : SProp := I : sTrue.
 
+(* The automatic generation of the fixpoint from the inductive definition *)
+(* as presented in the paper has been developed as a branch of the Equation plugin *)
+(* which is currently not well packaged. Thus, we provide directly the generated definitions. *)
+
 (* Derive Invert for le. *)
 
 Definition le : nat -> nat -> SProp := 
@@ -64,6 +68,8 @@ Inductive Divide : nat -> nat -> SProp:=
 | divide_0' : forall n, Divide n 0
 | divide_S' : forall n m (e: S n <= S m), Divide (S n) (m - n) -> Divide (S n) (S m).
 
+(* Again, we copy&paste the definitions generated by the Equation plugin *)
+
 (* Derive Invert for Divide.  *)
 
 Fixpoint invert_Divide var var0 {struct var0} : SProp :=
@@ -79,14 +85,6 @@ Fixpoint invert_Divide var var0 {struct var0} : SProp :=
 
 Infix "|" := invert_Divide (at level 80). 
 
-Goal 5 | 145.
-  cbn. repeat econstructor. 
-Defined.
-
-Goal (5 | 146) -> sFalse.
-  cbn. firstorder.
-Defined. 
-
 Definition divide_0 n : n | 0 := I. 
 
 Definition divide_S n m (e: S n <= S m) (H: S n | S m - S n) : S n | S m
@@ -104,6 +102,18 @@ Proof.
     exact (HS n n0 H.1 H.2 (divide_rect P H0 HS (S n) (n0 - n) H.2)).
 Defined. 
 
+Goal 5 | 145.
+  cbn. repeat econstructor. 
+Defined.
+
+Goal (5 | 146) -> sFalse.
+  cbn. firstorder.
+Defined. 
+
+
+(* Although we have definitional proof irrelevance for n | m, we can still extract the natural number 
+that witnesses the fact that n is a divisor of m out of the proof that n | m *)
+
 Definition divide_to_nat {n m} : n | m -> nat :=
   divide_rect (fun _ _ (_:_ | _) => nat) (fun _ => 0) (fun _ _ _ _ k => S k) n m.
 
@@ -120,30 +130,18 @@ Inductive is_gcd (a b g:nat) : SProp :=
   (g | a) -> (g | b) -> (forall x, (x | a) -> (x | b) -> (x | g)) ->
   is_gcd a b g.
 
-(* Derive Invert for is_gcd.  *)
-
-Definition invert_is_gcd : nat -> nat -> nat -> SProp :=
-fix invert_is_gcd (a b g : nat) {struct a} : SProp :=
-  {_ : g | a & {_ : g | b & forall x : nat, x | a -> x | b -> x | g}}.
-
+Definition rel_prime (a b:nat) : SProp := is_gcd a b 1.
 
-
-Definition rel_prime (a b:nat) : SProp := invert_is_gcd a b 1.
+(* This definition gives us definitional proof irrelevance for prime, without paying the price of the definition of a decision procedure into booleans 
+(for instance using the sieve of Eratosthenes) and a proof that it corresponds to primality *)
 
 Inductive prime (p:nat) : SProp :=
   prime_intro :
     1 < p -> (forall n, (1 <= n) -> (n < p) -> rel_prime n p) -> prime p.
 
-(* Derive Invert for prime. *)
-
-Definition invert_prime : nat -> SProp :=
-fix invert_prime (p : nat) : SProp :=
-  {_ : 2 <= p & forall n : nat, 1 <= n -> S n <= p -> rel_prime n p}.
-
-Goal invert_prime 13.
-  cbn. exists I. intro n. 
-  destruct n. intuition. intros _.
-  intro e. cbn in e.
+Goal prime 13.
+  cbn. econstructor. exact I. intro n. 
+  destruct n. inversion 1. intros _ e. cbn in e.
   repeat (try solve [firstorder];
       destruct n; [ cbn;  repeat econstructor; repeat (destruct x; firstorder) |]).
   firstorder.

SetoidCwf.v

@@ -1,5 +1,7 @@
 (* -*- coq-prog-args : ("-allow-sprop")-*-  *)
 
+(* This files requires some basic HoTT reasoning for equality *)
+
 Require Import MiniHoTT.