]> matita.cs.unibo.it Git - helm.git/commitdiff
...
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Apr 2007 14:29:38 +0000 (14:29 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 10 Apr 2007 14:29:38 +0000 (14:29 +0000)
helm/software/matita/library/decidable_kit/decidable.ma [new file with mode: 0644]
helm/software/matita/library/decidable_kit/eqtype.ma [new file with mode: 0644]
helm/software/matita/library/decidable_kit/fintype.ma [new file with mode: 0644]
helm/software/matita/library/decidable_kit/list_aux.ma [new file with mode: 0644]
helm/software/matita/library/decidable_kit/streicher.ma [new file with mode: 0644]

diff --git a/helm/software/matita/library/decidable_kit/decidable.ma b/helm/software/matita/library/decidable_kit/decidable.ma
new file mode 100644 (file)
index 0000000..3aaa4a6
--- /dev/null
@@ -0,0 +1,197 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/decidable_kit/decidable/".
+
+(* classical connectives for decidable properties *)
+
+include "decidable_kit/streicher.ma".
+include "datatypes/bool.ma".
+include "logic/connectives.ma".
+include "nat/compare.ma".
+(* se non includi connectives accade un errore in modo reproducibile*)
+
+(* ### Prop <-> bool reflection predicate and lemmas for switching ### *)
+inductive reflect (P : Prop) : bool  → Type ≝
+  | reflect_true : P → reflect P true
+  | reflect_false: ¬P → reflect P false.
+  
+lemma b2pT : ∀P,b. reflect P b → b = true → P.
+intros 3 (P b H); 
+(* XXX generalize in match H; clear H; rewrite > Db;*)
+(* la rewrite pare non andare se non faccio la generalize *)
+(* non va inversion: intros (H);inversion H; *)
+cases H; [intros; assumption | intros 1 (ABS); destruct ABS ]
+qed.
+
+lemma b2pF : ∀P,b. reflect P b → b = false → ¬P.
+intros 3 (P b H); 
+cases H; [intros 1 (ABS); destruct ABS| intros; assumption]
+qed.
+
+lemma p2bT : ∀P,b. reflect P b → P → b = true.
+intros 4 (P b H Hp);
+cases H (Ht Hf); [ intros; reflexivity | cases (Hf Hp)]
+qed.
+
+lemma p2bF : ∀P,b. reflect P b → ¬P → b = false.
+intros 4 (P b H Hp);
+cases H (Ht Hf); [ cases (Hp Ht) | reflexivity ]
+qed.
+
+lemma idP : ∀b:bool.reflect (b=true) b.
+intros (b); cases b; [ constructor 1; reflexivity | constructor 2;]
+unfold Not; intros (H); destruct H;
+qed.
+
+(* ### standard connectives/relations with reflection predicate ### *)
+
+definition negb : bool → bool ≝ λb.match b with [ true ⇒ false | false ⇒ true].
+
+lemma negbP : ∀b:bool.reflect (b = false) (negb b).
+intros (b); cases b; simplify; [apply reflect_false | apply reflect_true]
+[unfold Not; intros (H); destruct H | reflexivity]
+qed.  
+
+definition andb : bool → bool → bool ≝
+  λa,b:bool. match a with [ true ⇒ b | false ⇒ false ].
+  
+lemma andbP : ∀a,b:bool. reflect (a = true ∧ b = true) (andb a b).
+intros (a b); 
+generalize in match (refl_eq ? (andb a b));
+generalize in match (andb a b) in ⊢ (? ? ? % → %); intros 1 (c);
+cases c; intros (H); [ apply reflect_true | apply reflect_false ];
+generalize in match H; clear H;
+cases a; simplify; 
+[1: intros (E); rewrite > E; split; reflexivity
+|2: intros (ABS); destruct ABS
+|3: intros (E); rewrite > E; unfold Not; intros (ABS); decompose;  destruct H1
+|4: intros (E); unfold Not; intros (ABS); decompose; destruct H]
+qed.
+
+lemma andbPF : ∀a,b:bool. reflect (a = false ∨ b = false) (negb (andb a b)).
+intros (a b); cases a; cases b; simplify;
+[1: apply reflect_false | *: apply reflect_true ]
+[unfold Not; intros (H); cases H; destruct H1|right|left|left] reflexivity;
+qed.
+
+definition orb : bool → bool → bool ≝
+  λa,b.match a in bool with [true ⇒ true | false ⇒ b].
+  
+lemma orbP : ∀a,b:bool. reflect (a = true ∨ b = true) (orb a b).
+intros (a b); cases a; cases b; simplify;
+[1,2,3: apply reflect_true; [1,2: left | right ]; reflexivity 
+| apply reflect_false; unfold Not; intros (H); cases H (E E); destruct E]
+qed. 
+
+lemma orbC : ∀a,b. orb a b = orb b a.
+intros (a b); cases a; cases b; auto. qed.
+
+lemma lebP: ∀x,y. reflect (x ≤ y) (leb x y).
+intros (x y); generalize in match (leb_to_Prop x y); 
+cases (leb x y); simplify; intros (H); 
+[apply reflect_true | apply reflect_false ] assumption.
+qed. 
+
+lemma leb_refl : ∀n.leb n n = true.
+intros (n); apply (p2bT ? ? (lebP ? ?)); apply le_n; qed.
+
+lemma lebW : ∀n,m. leb (S n) m = true → leb n m = true.
+intros (n m H); lapply (b2pT ? ? (lebP ? ?) H); clear H;
+apply (p2bT ? ? (lebP ? ?)); auto.
+qed. 
+
+definition ltb ≝ λx,y.leb (S x) y.
+
+lemma ltbP: ∀x,y. reflect (x < y) (ltb x y). 
+intros (x y); apply (lebP (S x) y);
+qed.
+
+lemma ltb_refl : ∀n.ltb n n = false.
+intros (n); apply (p2bF ? ? (ltbP ? ?)); auto; 
+qed.
+    
+(* ### = between booleans as <-> in Prop ### *)    
+lemma eq_to_bool : 
+  ∀a,b:bool. a = b → (a = true → b = true) ∧ (b = true → a = true).
+intros (a b Eab); split; rewrite > Eab; intros; assumption;
+qed.
+lemma bool_to_eq : 
+  ∀a,b:bool. (a = true → b = true) ∧ (b = true → a = true) → a = b.
+intros (a b Eab); decompose;
+generalize in match H; generalize in match H1; clear H; clear H1;
+cases a; cases b; intros (H1 H2);
+[2: rewrite > (H2 ?) | 3: rewrite > (H1 ?)] reflexivity;
+qed.
+
+
+lemma leb_eqb : ∀n,m. orb (eqb n m) (leb (S n) m) = leb n m.
+intros (n m); apply bool_to_eq; split; intros (H);
+[1:cases (b2pT ? ? (orbP ? ?) H); [2: auto] 
+   rewrite > (eqb_true_to_eq ? ? H1); auto
+|2:cases (b2pT ? ? (lebP ? ?) H); 
+   [ elim n; [reflexivity|assumption] 
+   | simplify; rewrite > (p2bT ? ? (lebP ? ?) H1); rewrite > orbC ]
+   reflexivity]
+qed.
+
+
+(* OUT OF PLACE *)
+lemma ltW : ∀n,m. n < m → n < (S m). intros; auto. qed.
+
+lemma ltbW : ∀n,m. ltb n m = true → ltb n (S m) = true.
+intros (n m H); letin H1 ≝ (b2pT ? ? (ltbP ? ?) H); clearbody H1;
+apply (p2bT ? ? (ltbP ? ?) (ltW ? ? H1));
+qed.
+
+lemma ltS : ∀n,m.n < m → S n < S m.
+intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H);
+qed.
+
+lemma ltS' : ∀n,m.S n < S m → n < m.
+intros (n m H); apply (b2pT ? ? (ltbP ? ?)); simplify; apply (p2bT ? ? (ltbP ? ?) H);
+qed.
+
+lemma ltb_n_Sm : ∀m.∀n:nat. (orb (ltb n m) (eqb n m)) = ltb n (S m).
+intros (m n); apply bool_to_eq; split;
+[1: intros; cases (b2pT ? ? (orbP ? ?) H); [1: apply ltbW; assumption]
+    rewrite > (eqb_true_to_eq ? ? H1); simplify; 
+    rewrite > leb_refl; reflexivity  
+|2: generalize in match m; clear m; elim n 0;
+    [1: simplify; intros; cases n1; reflexivity;
+    |2: intros 1 (m); elim m 0;
+        [1: intros; apply (p2bT ? ? (orbP ? ?));
+            lapply (H (pred n1) ?); [1: reflexivity] clear H;
+            generalize in match H1; 
+            generalize in match Hletin;
+            cases n1; [1: simplify; intros; destruct H2]
+            intros; unfold pred in H; simplify in H;
+            cases (b2pT ? ? (orbP ? ?) H); [left|right] assumption; 
+        |2: clear m; intros (m IH1 IH2 w);
+            lapply (IH1 ? (pred w));
+            [3: generalize in match H; cases w; [2: intros; assumption]
+                simplify; intros; destruct H1;
+            |1: intros; apply (IH2 (S n1)); assumption;
+            |2: generalize in match H; generalize in match Hletin; 
+                cases w; [1: simplify; intros; destruct H2]
+                intros (H H1); cases (b2pT ? ? (orbP ? ?) H);
+                apply (p2bT ? ? (orbP ? ?));[left|right] assumption]]]]
+qed.
+        
+(* non mi e' chiaro a cosa serva ... *)
+lemma congr_S : ∀n,m.n = m → S n = S m.
+intros 1; cases n; intros; rewrite > H; reflexivity.
+qed.
diff --git a/helm/software/matita/library/decidable_kit/eqtype.ma b/helm/software/matita/library/decidable_kit/eqtype.ma
new file mode 100644 (file)
index 0000000..7b0f94e
--- /dev/null
@@ -0,0 +1,170 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/decidable_kit/eqtype/".
+
+include "decidable_kit/decidable.ma".
+include "datatypes/constructors.ma".
+
+(* ### types with a decidable AND rewrite (leibniz) compatible ### *)
+
+definition eq_compatible ≝ λT:Type.λa,b:T. reflect (a = b).
+    
+record eqType : Type ≝ {
+  sort :> Type;
+  cmp : sort → sort → bool ;
+  eqP : ∀x,y:sort. eq_compatible sort x y (cmp x y)
+}.
+
+lemma cmp_refl : ∀d:eqType.∀x. cmp d x x = true.
+intros (d x); generalize in match (eqP d x x); intros (H);
+unfold in H; (* inversion non fa whd!!! *)
+inversion H; [ intros; reflexivity | intros (ABS); cases (ABS (refl_eq ? ?)) ]
+qed. 
+
+(* to use streicher *)
+lemma eqType_decidable : ∀d:eqType. decT d.
+intros (d); unfold decT; intros (x y); unfold decidable;
+generalize in match (eqP d x y); intros (H);
+cases H; [left | right] assumption;
+qed.
+
+lemma eqbP : ∀x,y:nat. eq_compatible nat x y (eqb x y).
+intros (x y);
+generalize in match (refl_eq ? (eqb x y));
+generalize in match (eqb x y) in ⊢ (? ? ? % → %); intros 1 (b);
+cases b; intros (H); [ apply reflect_true | apply reflect_false ];
+[ apply (eqb_true_to_eq ? ? H) | apply (eqb_false_to_not_eq ? ? H) ]
+qed.
+
+definition nat_eqType : eqType ≝ mk_eqType ? ? eqbP.
+(* XXX le coercion nel cast non vengono inserite *)
+definition nat_canonical_eqType : nat → nat_eqType := 
+  λn : nat.(n : sort nat_eqType).
+coercion cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con.
+
+definition bcmp ≝ λx,y:bool. match x with [ true ⇒ y | false => notb y ].
+
+lemma bcmpP : ∀x,y:bool. eq_compatible bool x y (bcmp x y).
+intros (x y);
+generalize in match (refl_eq ? (bcmp x y));
+generalize in match (bcmp x y) in ⊢ (? ? ? % → %); intros 1 (b);
+cases b; intros (H); [ apply reflect_true | apply reflect_false ];
+generalize in match H; clear H;
+cases x; cases y; simplify; intros (H); [1,4: reflexivity];
+(* non va: try destruct H; *)
+[1,2,3,6: destruct H | *: unfold Not; intros (H1); destruct H1]
+qed.
+
+definition bool_eqType : eqType ≝  mk_eqType ? ? bcmpP.
+definition bool_canonical_eqType : bool → bool_eqType := 
+  λb : bool.(b : sort bool_eqType).
+coercion cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con.
+
+(* ### subtype of an eqType ### *)
+
+record sigma (d : eqType) (p : d -> bool) : Type ≝ {
+  sval : d;
+  sprop : p sval = true
+}.
+
+notation "{x, h}"
+  right associative with precedence 80
+for @{'sig $x $h}.
+
+interpretation "sub_eqType" 'sig x h = 
+  (cic:/matita/decidable_kit/eqtype/sigma.ind#xpointer(1/1/1) _ _ x h).
+
+(* restricting an eqType gives an eqType *)
+lemma sigma_eq_dec : ∀d:eqType.∀p.∀x,y:sigma d p. 
+  eq_compatible ? x y (cmp ? (sval ? ? x) (sval ? ?y)).
+intros (d p x y);
+generalize in match (refl_eq ? (cmp d (sval d p x) (sval d p y)));
+generalize in match (cmp d (sval d p x) (sval d p y)) in ⊢ (? ? ? % → %); intros 1 (b);
+cases b; cases x (s ps); cases y (t pt); simplify; intros (Hcmp);
+[ constructor 1;
+  generalize in match (eqP d s t); intros (Est);
+  cases Est (H); clear Est;
+  [ generalize in match ps;
+    rewrite > H; intros (pt'); 
+    rewrite < (pirrel bool (p t) true pt pt' (eqType_decidable bool_eqType));
+    reflexivity;
+  | cases (H (b2pT ? ? (eqP d s t) Hcmp))
+  ]
+| constructor 2; unfold Not; intros (H);
+  (* XXX destruct H; *)
+  change in Hcmp with (cmp d (match {?,ps} with [(mk_sigma s _)⇒s]) t = false);
+  rewrite > H in Hcmp; simplify in Hcmp; rewrite > cmp_refl in Hcmp; destruct Hcmp;
+]
+qed. 
+
+definition sub_eqType ≝ λd : eqType.λp. mk_eqType ? ? (sigma_eq_dec d p).
+
+inductive in_sub (d : eqType) (p : d → bool) (x : d) : option (sigma d p) → Type ≝
+| in_sig : ∀s : sigma d p. sval ? ? s = x → in_sub d p x (Some ? s)
+| out_sig : p x = false → in_sub d p x (None ?).
+
+definition if_p ≝ λd:eqType.λp:d→bool.λx:d. 
+  match (eqP bool_eqType (p x) true) with 
+  [ (reflect_true H) ⇒ Some ? {?,H} 
+  | (reflect_false _) ⇒ None ?].
+
+lemma in_sub_eq : ∀d,p,x. in_sub d p x (if_p d p x).
+intros (d p x); unfold if_p;
+cases (eqP bool_eqType (p x) true); simplify;
+[ apply in_sig; reflexivity; | apply out_sig; apply (p2bF ? ? (idP ?) H)]
+qed.  
+
+definition ocmp : ∀d:eqType.∀a,b:option d.bool ≝
+  λd:eqType.λa,b:option d.
+  match a with 
+  [ None ⇒ match b with [ None ⇒ true | (Some _) ⇒ false] 
+  | (Some x) ⇒ match b with [ None ⇒ false | (Some y) ⇒ cmp d x y]].  
+  
+lemma ocmpP : ∀d:eqType.∀a,b:option d.eq_compatible ? a b (ocmp d a b).
+intros (d a b);
+generalize in match (refl_eq ? (ocmp ? a b));
+generalize in match (ocmp ? a b) in ⊢ (? ? ? % → %); intros 1 (c);
+cases c; intros (H); [ apply reflect_true | apply reflect_false ];
+generalize in match H; clear H;
+cases a; cases b;
+[1: intros; reflexivity;
+|2,3: intros (H); destruct H;
+|4: intros (H); simplify in H; rewrite > (b2pT ? ? (eqP d ? ?) H); reflexivity; 
+    (* se faccio la rewrite diretta non tipa *)
+|5: intros (H H1); destruct H
+|6,7: unfold Not; intros (H H1); destruct H1
+|8: unfold Not; simplify; intros (H H1); 
+    (* ancora injection non va *)
+    cut (s = s1); [ rewrite > Hcut in H;  rewrite > cmp_refl in H;  destruct H;].
+    change with (match (Some d s) with
+                 [ None ⇒ s | (Some s) ⇒ s] = s1); rewrite > H1;
+                 simplify; reflexivity;
+] qed.
+
+definition option_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (ocmpP d).
+definition option_canonical_eqType : ∀d:eqType.d → option_eqType d ≝
+  λd:eqType.λx:d.(Some ? x : sort (option_eqType d)).
+coercion cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con.
+
+(* belle le coercions! *)
+definition test_canonical_option_eqType ≝ 
+  (eq (option_eqType nat_eqType) O (S O)).
+
+(* OUT OF PLACE *)       
+lemma eqbC : ∀x,y:nat. eqb x y = eqb y x.
+intros (x y); apply bool_to_eq; split; intros (H); 
+rewrite > (b2pT ? ? (eqbP ? ?) H); rewrite > (cmp_refl nat_eqType);
+reflexivity;
+qed.
diff --git a/helm/software/matita/library/decidable_kit/fintype.ma b/helm/software/matita/library/decidable_kit/fintype.ma
new file mode 100644 (file)
index 0000000..c3e5ba4
--- /dev/null
@@ -0,0 +1,147 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/decidable_kit/fintype/".
+
+include "decidable_kit/eqtype.ma".
+include "decidable_kit/list_aux.ma".
+
+record finType : Type ≝ {
+  fsort :> eqType;
+  enum : list fsort;
+  enum_uniq : ∀x:fsort. count fsort (cmp fsort x) enum = (S O)  
+}.
+
+definition segment : nat → eqType ≝ 
+  λn.sub_eqType nat_eqType (λx:nat_eqType.ltb x n).
+
+definition is_some : ∀d:eqType. option d → bool ≝ 
+  λd:eqType.λo:option d.notb (cmp (option_eqType d) (None ?) o).
+
+definition filter ≝
+  λA,B:Type.λp:A→option B.λl:list A.
+  foldr A ? 
+    (λx,acc. match (p x) with [None ⇒ acc | (Some y) ⇒ cons B y acc]) (nil B) l.
+
+definition segment_enum  ≝
+  λbound.filter ? ? (if_p nat_eqType (λx.ltb x bound)) (iota O bound).
+
+lemma iota_ltb : ∀x,p:nat. mem nat_eqType x (iota O p) = ltb x p.
+intros (x p); elim p; simplify; [1:reflexivity]
+rewrite < leb_eqb;
+generalize in match (refl_eq ? (cmp ? x n));
+generalize in match (cmp ? x n) in ⊢ (? ? % ? → %); intros 1 (b);
+cases b; simplify; intros (H1); [1: reflexivity]
+rewrite > H; fold simplify (ltb x n); rewrite > H1; reflexivity;
+qed.
+
+lemma mem_filter :
+  ∀d1,d2:eqType.(*∀y:d1.*)∀x:d2.∀l:list d1.∀p:d1 → option d2.
+  (∀y.mem d1 y l = true → 
+    match (p y) with [None ⇒ false | (Some q) ⇒ cmp d2 x q] = false) →
+  mem d2 x (filter d1 d2 p l) = false.
+intros 5 (d1 d2 x l p); 
+elim l; [1: simplify; auto]
+simplify; fold simplify (filter d1 d2 p l1);
+generalize in match (refl_eq ? (p t));
+generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+[1: simplify; intros (Hpt); apply H; intros (y Hyl);
+  apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1));
+  rewrite > Hyl; rewrite > orbC; reflexivity;
+|2:simplify; intros (Hpt); 
+  generalize in match (refl_eq ? (cmp ? x s));
+  generalize in match (cmp ? x s) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+  [1: simplify; intros (Exs);
+      rewrite < (H1 t); [2: simplify; rewrite > cmp_refl; reflexivity;]
+      rewrite > Hpt; simplify; symmetry; assumption;
+  |2: intros (Dxs); simplify; apply H; intros;
+      apply H1; simplify; fold simplify (orb (cmp ? y t) (mem ? y l1));
+      rewrite > H2; rewrite > orbC; reflexivity;]]
+qed.
+  
+lemma count_O : 
+  ∀d:eqType.∀p:d→bool.∀l:list d. 
+    (∀x:d.mem d x l = true → notb (p x) = true) → count d p l = O.
+intros 3 (d p l); elim l; simplify; [1: reflexivity]
+fold simplify (count d p l1); (* XXX simplify troppo *)
+generalize in match (refl_eq ? (p t));
+generalize in match (p t) in ⊢ (? ? ? % → %); intros 1 (b);
+cases b; simplify; 
+[2:intros (Hpt); apply H; intros; apply H1; simplify;
+   generalize in match (refl_eq ? (cmp d x t));
+   generalize in match (cmp d x t) in ⊢ (? ? ? % → %); intros 1 (b1);
+   cases b1; simplify; intros; [2:rewrite > H2] auto.
+|1:intros (H2); lapply (H1 t); [2:simplify; rewrite > cmp_refl; simplify; auto]
+   rewrite > H2 in Hletin; simplify in Hletin; destruct Hletin]
+qed.    
+    
+lemma segment_finType : nat → finType.
+intros (bound); 
+letin fsort ≝ (segment bound);
+letin enum ≝ (segment_enum bound);
+cut (∀x:fsort. count fsort (cmp fsort x) enum = (S O));
+ [ apply (mk_finType fsort enum Hcut)
+ | intros (x); cases x (n Hn); simplify in Hn; clear x;
+   generalize in match Hn; generalize in match Hn; clear Hn;
+   unfold segment_enum;
+   generalize in match bound in ⊢ (% → ? → ? ? (? ? ? (? ? ? ? %)) ?);
+   intros 1 (m); elim m  (Hm Hn p IH Hm Hn);
+   [ destruct Hm;
+   | simplify; cases (eqP bool_eqType (ltb p bound) true); simplify;
+     (* XXX simplify che spacca troppo *)
+     fold simplify (filter nat_eqType (sigma nat_eqType (λx.ltb x bound))
+                     (if_p nat_eqType (λx.ltb x bound)) (iota O p));
+     [1:unfold segment in ⊢ (? ? match ? % ? ? with [true⇒ ?|false⇒ ?] ?);
+        unfold nat_eqType in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
+        simplify in ⊢ (? ? match % with [true⇒ ?|false⇒ ?] ?);
+        generalize in match (refl_eq ? (eqb n p));
+        generalize in match (eqb n p) in ⊢ (? ? ? % → %); intros 1(b);
+        cases b; simplify;
+        [2:intros (Enp); rewrite > IH; [1,3: auto]
+           rewrite <  ltb_n_Sm in Hm; rewrite > Enp in Hm;
+           generalize in match Hm; cases (ltb n p); intros; [1:reflexivity]
+           simplify in H1; destruct H1;
+        |1:clear IH; intros (Enp); 
+           fold simplify (count fsort (cmp fsort {n, Hn})
+                           (filter ? (sigma nat_eqType (λx.ltb x bound))
+                           (if_p nat_eqType (λx.ltb x bound)) (iota O p)));
+           rewrite > (count_O fsort); [1: reflexivity]
+           intros 1 (x);
+           rewrite < (b2pT ? ? (eqP ? n ?) Enp);
+           cases x (y Hy); intros (ABS); clear x;
+           unfold segment; unfold notb; simplify; 
+           generalize in match (refl_eq ? (cmp ? n y));
+           generalize in match (cmp ? n y) in ⊢ (? ? ? % → %); intros 1 (b); cases b; clear b;
+           intros (Eny); simplify; [2: auto]
+           rewrite < ABS; symmetry; clear ABS;
+           generalize in match Hy; clear Hy; rewrite < (b2pT ? ? (eqP nat_eqType ? ?) Eny);
+           simplify; intros (Hn); fold simplify (iota O n);
+           apply (mem_filter nat_eqType fsort);
+           intros (w Hw);
+           fold simplify (sort nat_eqType);
+           cases (in_sub_eq nat_eqType (λx:nat_eqType.ltb x bound) w);
+           simplify; [2: reflexivity]
+           generalize in match H1; clear H1; cases s; clear s; intros (H1);
+           unfold segment; simplify; simplify in H1; rewrite > H1;
+           rewrite > iota_ltb in Hw;
+           apply (p2bF ? ? (eqP nat_eqType ? ?));
+           unfold Not; intros (Enw);
+           rewrite > Enw in Hw; rewrite > ltb_refl in Hw; destruct Hw]
+     |2:rewrite > IH; [1:reflexivity|3:assumption]
+          rewrite <  ltb_n_Sm in Hm;
+          cases (b2pT ? ?(orbP ? ?) Hm);[1: assumption]
+          rewrite > (b2pT ? ? (eqbP ? ?) H1) in Hn;
+          rewrite > Hn in H; cases (H ?); reflexivity;
+     ]]]      
+qed.
diff --git a/helm/software/matita/library/decidable_kit/list_aux.ma b/helm/software/matita/library/decidable_kit/list_aux.ma
new file mode 100644 (file)
index 0000000..8f30d3f
--- /dev/null
@@ -0,0 +1,123 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/decidable_kit/list_aux/".
+
+include "list/list.ma".
+include "decidable_kit/eqtype.ma".
+include "nat/plus.ma".
+
+(* ### some functions on lists (some can be moved to list.ma ### *)
+
+let rec foldr (A,B:Type) (f : A → B → B) (b : B) (l : list A) on l : B := 
+  match l with [ nil ⇒ b | (cons a l) ⇒ f a (foldr ? ? f b l)].
+   
+definition length ≝ λT:Type.λl:list T.foldr T nat (λx,c.S c) O l.
+
+definition count : ∀T : eqType.∀f : T → bool.∀l : list T. nat :=
+  λT:eqType.λf,l. 
+  foldr T nat (λx,acc. match (f x) with [ true ⇒ S acc | false ⇒ acc ]) O l.
+     
+let rec mem (d : eqType) (x : d) (l : list d) on l : bool ≝
+  match l with
+  [ nil ⇒ false 
+  | cons y tl ⇒
+     match (cmp d x y) with [ true ⇒ true | false ⇒ mem d x tl]].
+
+definition iota : nat → nat → list nat ≝
+  λn,m. nat_rect (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m.
+  
+let rec map (A,B:Type) (f: A → B) (l : list A) on l : list B ≝
+  match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
+
+(* ### induction principle for functions visiting 2 lists in parallel *)
+lemma list_ind2 : 
+  ∀T1,T2:Type.∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
+  length ? l1 = length ? l2 →
+  (P (nil ?) (nil ?)) → 
+  (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → 
+  P l1 l2.
+intros (T1 T2 l1 l2 P Hl Pnil Pcons);
+generalize in match Hl; clear Hl;
+generalize in match l2; clear l2;
+elim l1 1 (l2 x1); [ cases l2; intros (Hl); [assumption| destruct Hl]
+| intros 3 (tl1 IH l2); cases l2; [1: simplify; intros 1 (Hl); destruct Hl] 
+  intros 1 (Hl); apply Pcons;
+  apply IH; destruct Hl; 
+  (* XXX simplify in Hl non folda length *) 
+  assumption;]
+qed.
+  
+lemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
+intros (A B f g l Efg); elim l; simplify; [1: reflexivity ];
+rewrite > (Efg t); rewrite > H; reflexivity;  
+qed.
+
+(* ### eqtype for lists ### *)
+let rec lcmp (d : eqType) (l1,l2 : list d) on l1 : bool ≝
+  match l1 with
+  [ nil ⇒ match l2 with [ nil ⇒ true | (cons _ _) ⇒ false]
+  | (cons x1 tl1) ⇒ match l2 with 
+      [ nil ⇒ false | (cons x2 tl2) ⇒ andb (cmp d x1 x2) (lcmp d tl1 tl2)]].
+           
+lemma lcmp_length : 
+  ∀d:eqType.∀l1,l2:list d.
+ lcmp ? l1 l2 = true → length ? l1 = length ? l2.
+intros 2 (d l1); elim l1 1 (l2 x1);
+[ cases l2; simplify; intros;[reflexivity|destruct H] 
+| intros 3 (tl1 IH l2); cases (l2); intros; [1:destruct H]
+  simplify; (* XXX la apply non fa simplify? *) 
+  apply congr_S; apply (IH l);
+  (* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *)
+  simplify in H;
+  letin H' ≝ (b2pT ? ? (andbP ? ?) H); decompose; assumption]
+qed.
+
+lemma lcmpP : ∀d:eqType.∀l1,l2:list d. eq_compatible (list d) l1 l2 (lcmp d l1 l2).
+intros (d l1 l2);
+generalize in match (refl_eq ? (lcmp d l1 l2));
+generalize in match (lcmp d l1 l2) in ⊢ (? ? ? % → %); intros 1 (c);
+cases c; intros (H); [ apply reflect_true | apply reflect_false ]
+[ letin Hl≝ (lcmp_length ? ? ? H); clearbody Hl;
+  generalize in match H; clear H;
+  apply (list_ind2 ? ? ? ? ? Hl); [1: intros; reflexivity]
+  simplify; intros (tl1 tl2 hd1 hd2 IH H);
+  letin H' ≝ (b2pT ? ? (andbP ? ?) H); decompose;
+  rewrite > (IH H2); rewrite > (b2pT ? ? (eqP d ? ?) H1); reflexivity
+| generalize in match H; clear H; generalize in match l2; clear l2;
+  elim l1 1 (l1 x1);
+   [ cases l1; [intros; destruct H]
+     unfold Not; intros; destruct H1;
+   | intros 3 (tl1 IH l2); cases l2;
+     [ unfold Not; intros; destruct H1;
+     | simplify;  intros;
+       letin H' ≝ (p2bT ? ? (negbP ?) H); clearbody H'; clear H;
+       letin H'' ≝ (b2pT ? ? (andbPF ? ?) H'); clearbody H''; clear H';
+       cases H''; clear H'';
+       [ intros; 
+         letin H' ≝ (b2pF ? ? (eqP d ? ?) H); clearbody H'; clear H;
+         (* XXX destruct H1; *)
+         change in H' with (Not ((match (x1::tl1) with [nil⇒x1|(cons x1 _) ⇒ x1]) = s));
+         rewrite > H1 in H'; simplify in H'; apply H'; reflexivity;
+       | intros; 
+         letin H' ≝ (IH ? H); clearbody H';
+         (* XXX destruct H1 *)
+         change in H' with (Not ((match (x1::tl1) with [nil⇒tl1|(cons _ l) ⇒ l]) = l)); 
+         rewrite > H1 in H'; simplify in H'; apply H'; reflexivity;
+       ]]]]
+qed.
+    
+definition list_eqType : eqType → eqType ≝ λd:eqType.mk_eqType ? ? (lcmpP d).  
+  
diff --git a/helm/software/matita/library/decidable_kit/streicher.ma b/helm/software/matita/library/decidable_kit/streicher.ma
new file mode 100644 (file)
index 0000000..83c6f61
--- /dev/null
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/decidable_kit/streicher/".
+
+include "logic/connectives.ma".
+include "logic/equality.ma".
+
+definition step ≝ λT:Type.λa,b,c:T.λH1:a=b.λH2:a=c. eq_ind T ? (λx.b = x) H1 ? H2.
+
+lemma stepH : ∀T:Type.∀a:T.∀H:a=a. step ? ? ? ? H H = refl_eq T a.
+intros (T a H); cases H; reflexivity.
+qed.
+
+definition decT ≝ λT:Type.∀x,y:T. decidable (x=y).
+
+lemma nu : ∀T:Type.∀a,b:T. decT T → ∀E:a=b. a=b.
+intros (T a b decT E); cases (decT a b) (Ecanonical Abs); [ exact Ecanonical | cases (Abs E) ]
+qed.
+
+lemma nu_k : ∀T:Type.∀a,b:T.∀E1,E2:a=b. ∀d : decT T. nu ? ? ? d E1 = nu ? ? ? d E2.
+intros (T a b E1 E2 decT); unfold nu; 
+cases (decT a b); simplify; [ reflexivity | cases (H E1) ]
+qed.
+
+definition nu_inv ≝ λT:Type.λa,b:T. λd: decT T.λE:a=b. 
+  step ? ? ? ? (nu ? ? ? d (refl_eq ? a)) E. 
+
+definition cancel ≝ λT:Type.λA,B:Type.λf.λg:A→B.∀x:A.f (g x) = x.
+
+(* non inferisce Prop?!??! *)
+lemma cancel_nu_nu_inv : ∀T:Type.∀a,b:T.∀d: decT T. 
+  cancel Prop (a=b) (a=b) (nu_inv ? a b d) (nu ? a b d).
+intros (T a b); unfold cancel; intros (E); cases E;
+unfold nu_inv; rewrite > stepH; reflexivity.
+qed.
+
+theorem pirrel :  ∀T:Type.∀a,b:T.∀E1,E2:a=b.∀d: decT T. E1 = E2.
+intros (T a b E1 E2 decT);
+rewrite < (cancel_nu_nu_inv ? ? ? decT); 
+rewrite < (cancel_nu_nu_inv ? ? ? decT) in ⊢ (? ? ? %);
+rewrite > (nu_k ? ? ? E1 E2 decT).
+reflexivity.
+qed.
+