--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+
projects / helm.git / commitdiff