green

Author: gert-smolka

coq/indind.v

@@ -4,12 +4,21 @@ From Coq Require Import Lia.
 (*** Inductive Equality *)
 Module IndEquality.
 
-  Inductive eq X (x: X) | : X -> Prop :=
-  | Q : eq x.
+  Inductive eq X (x: X) : X -> Prop :=
+  | Q : eq X x x.
 
   Check eq.
   Check Q.
 
+  
+  Definition E 
+    : forall X  (x: X) (p: X -> Type),  p x -> forall y, eq X x y -> p y
+    := fun X x p a _ e =>
+         match e with
+         | Q _ _ => a
+         end.
+
+
   Definition R 
     : forall X  (x y: X) (p: X -> Type),  eq X x y -> p x -> p y
     := fun X x _ p e => match e with
@@ -24,18 +33,18 @@ Section Star.
   Variable X : Type.
   Implicit Type R: X -> X -> Prop.
 
-  Inductive star R | (x : X) : X -> Prop :=
-  | Nil : star x x
-  | Cons y z : R x y -> star y z -> star x z.
+  Inductive star (R: X -> X -> Prop) (x: X) : X -> Prop :=
+  | Nil : star R x x
+  | Cons y z : R x y -> star R y z -> star R x z.
 
   Definition elim R (p: X -> X -> Prop)
     : (forall x, p x x) ->
       (forall x y z, R x y -> p y z -> p x z) -> 
       forall x y, star R x y -> p x y
-    := fun e1 e2 => fix f x _ a :=
+    := fun f1 f2 => fix f x _ a :=
       match a with
-      | Nil _ _ => e1 x
-      | Cons _ _ x' z r a => e2 x x' z r (f x' z a)
+      | Nil _ _ => f1 x
+      | Cons _ _ x' z r a => f2 x x' z r (f x' z a)
       end.
 
   Implicit Type p: X -> X -> Prop.
@@ -69,7 +78,7 @@ Section Star.
   Proof.
     induction 1 as [|x x' y r _ IH].
     - easy.
-    - intros H%IH. revert r H. apply Cons.
+    - intros H%IH. econstructor. exact r. exact H.
   Qed.
 
   Fact least R p :
@@ -119,9 +128,9 @@ End Star.
 (*** Inductive Comparisons *)
 
 Module LE.
-  Inductive le (x: nat) | : nat -> Prop :=
-  | leE : le x
-  | leS y : le y -> le (S y).
+  Inductive le (x: nat) : nat -> Prop :=
+  | leE : le x x 
+  | leS y : le x y -> le x (S y).
 
   Definition elim (x: nat) (p: nat -> Prop)
     : p x ->

coq/more.v

@@ -17,6 +17,13 @@ Notation "'Sigma' x .. y , p" :=
      format "'[' 'Sigma'  '/  ' x  ..  y ,  '/  ' p ']'")
     : type_scope.
 
+Fact skolem_trans {X Y} (p: X -> Y -> Prop) :
+  (forall x, Sigma y, p x y) -> Sigma f, forall x, p x (f x).
+Proof.
+  intros F.
+  exists (fun x => pi1 (F x)). intros x. exact (pi2 (F x)).
+Qed.
+
 (*** Injections and Bijections *)
 
 
@@ -256,39 +263,6 @@ Proof.
   - right. congruence.
 Qed.
 
-Fact R {X Y f g} :
-  @inv (option X) (option Y) g f ->
-  forall x, Sigma z, match f (Some x) with Some y => z = y | None => Some z = f None end.
-Proof.
-  intros H x.
-  destruct (f (Some x)) as [y|] eqn:E1.
-  - exists y. reflexivity.
-  - destruct (f None) as [y|] eqn:E2.
-    + exists y. reflexivity.
-    + exfalso. congruence.
-Qed.
-
-Fact R_inv {X Y f g} :
-  forall (H1: @inv (option X) (option Y) g f)
-    (H2: inv f g),
-    inv (fun y => pi1 (R H2 y)) (fun x => pi1 (R H1 x)).
-Proof.
-  intros H1 H2 x.
-  destruct (R H1 x) as [y H3]; cbn.
-  destruct (R H2 y) as [x' H4]; cbn.
-  revert H3 H4.  
-  destruct (f (Some x)) as [y1|] eqn:E.
-  - intros <-. rewrite <-E, H1. easy.
-  - intros ->.  rewrite H1. rewrite <-E, H1. congruence.
-Qed.
-
-Theorem bijection_option X Y : 
-  bijection (option X) (option Y) -> bijection X Y.
-Proof.
-  intros [f g H1 H2].
-  exists (fun y => pi1 (R H1 y)) (fun x => pi1 (R H2 x)); apply R_inv.
-Qed.
-
 Goal forall X Y, bijection X Y -> bijection (option X) (option Y).
 Proof.
   intros X Y [f g H1 H2].
@@ -298,70 +272,59 @@ Proof.
   - hnf. intros [y|]; congruence.
 Qed.
 
-Fact skolem_trans {X Y} (p: X -> Y -> Prop) :
-  (forall x, Sigma y, p x y) -> Sigma f, forall x, p x (f x).
+Definition lower' X Y (f: option X -> option Y) x z :=
+  match f (Some x) with
+  | Some y => z = y
+  | None => match f None with
+           | Some y => z = y
+           | None => False
+           end
+  end.
+
+Definition lower X Y (f: option X -> option Y) f' :=
+  forall x, lower' X Y f x (f' x).
+  
+Fact lower_sig {X Y} f :
+  injective f -> sig (lower X Y f).
 Proof.
-  intros F.
-  exists (fun x => pi1 (F x)). intros x. exact (pi2 (F x)).
+  intros H.
+  apply skolem_trans.
+  intros x. unfold lower'.
+  destruct (f (Some x)) as [y|] eqn:E1.
+  - eauto.
+  - destruct (f None) as [y|] eqn:E2.
+    + eauto.
+    + enough (Some x = None) by easy.
+      apply H. congruence.
 Qed.
-
-Module Version2024.
 
-  Definition lower' X Y (f: option X -> option Y) x z :=
-    match f (Some x) with
-    | Some y => z = y
-    | None => match f None with
-             | Some y => z = y
-             | None => False
-             end
-    end.
-
-  Definition lower X Y (f: option X -> option Y) f' :=
-    forall x, lower' X Y f x (f' x).
+Fact lem_lower X Y f g f' g'  :
+  inv g f -> inv f g ->
+  lower X Y f f' -> lower Y X g g' -> inv g' f'.
+Proof.
+  intros H1 H2 H3 H4 x.
+  specialize (H3 x). unfold lower' in H3.
+  destruct (f (Some x)) as [y|] eqn:E1.
+  - specialize (H4 y). unfold lower' in H4.
+    destruct (g (Some y)) as [x'|] eqn:E2; congruence.
+  - destruct (f None) as [y|] eqn:E2. 2:easy.
+    specialize (H4 y). unfold lower' in H4.
+    assert (E3: g (Some y) = None) by congruence.
+    rewrite E3 in H4.  
+    destruct (g None) as [x'|] eqn:E4; congruence.
+Qed.
 
-  
-  Fact lower_sig {X Y} f :
-    injective f -> sig (lower X Y f).
-  Proof.
-    intros H.
-    apply skolem_trans.
-    intros x. unfold lower'.
-    destruct (f (Some x)) as [y|] eqn:E1.
-    - eauto.
-    - destruct (f None) as [y|] eqn:E2.
-      + eauto.
-      + enough (Some x = None) by easy.
-        apply H. congruence.
-  Qed.
-  
-  Fact lem_lower X Y f g f' g'  :
-    inv g f -> inv f g ->
-    lower X Y f f' -> lower Y X g g' -> inv g' f'.
-  Proof.
-    intros H1 H2 H3 H4 x.
-    specialize (H3 x). unfold lower' in H3.
-    destruct (f (Some x)) as [y|] eqn:E1.
-    - specialize (H4 y). unfold lower' in H4.
-      destruct (g (Some y)) as [x'|] eqn:E2; congruence.
-    - destruct (f None) as [y|] eqn:E2. 2:easy.
-      specialize (H4 y). unfold lower' in H4.
-      assert (E3: g (Some y) = None) by congruence.
-      rewrite E3 in H4.  
-      destruct (g None) as [x'|] eqn:E4; congruence.
-  Qed.
+Theorem bijection_option X Y : 
+  bijection (option X) (option Y) -> bijection X Y.
+Proof.
+  intros [f g H1 H2].
+  destruct (lower_sig f) as [f' H3].
+  { eapply inv_injective, H1. }
+  destruct (lower_sig g) as [g' H4].
+  { eapply inv_injective, H2. }
+  exists f' g'; eapply lem_lower; eassumption.
+Qed.
 
-  Theorem bijection_option X Y : 
-    bijection (option X) (option Y) -> bijection X Y.
-  Proof.
-    intros [f g H1 H2].
-    destruct (lower_sig f) as [f' H3].
-    { eapply inv_injective, H1. }
-    destruct (lower_sig g) as [g' H4].
-    { eapply inv_injective, H2. }
-    exists f' g'; eapply lem_lower; eassumption.
-  Qed.
-End Version2024.
-     
 (*** Numeral Types *)
 
 Fixpoint num n : Type :=