From 6044e9411b4f174f382e9594fadacb40bb23c175 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 13 Oct 2009 14:57:30 +0000 Subject: [PATCH] Experimental scripts for nth-order rewriting principles. --- .../matita/nlibrary/logic/destruct_bb.ma | 82 ++++++ helm/software/matita/tests/destruct_bb.ma | 256 ++++++++++++++++++ 2 files changed, 338 insertions(+) create mode 100644 helm/software/matita/nlibrary/logic/destruct_bb.ma create mode 100644 helm/software/matita/tests/destruct_bb.ma diff --git a/helm/software/matita/nlibrary/logic/destruct_bb.ma b/helm/software/matita/nlibrary/logic/destruct_bb.ma new file mode 100644 index 000000000..d3d2aadc3 --- /dev/null +++ b/helm/software/matita/nlibrary/logic/destruct_bb.ma @@ -0,0 +1,82 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) +(* +include "nat/nat.ma". +include "list/list.ma". + +inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝ +| il_s : ∀n.T n → index_list T n n +| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n. + +lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p). + ∀m',n'.S m' = m → S n' = n → index_list T m' n'. +intros 5;elim i +[destruct;apply il_s;apply f;assumption +|apply il_c + [apply f;rewrite > H;assumption + |apply f1 + [rewrite > H;reflexivity + |assumption]]] +qed. + +definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝ + λT0:Type.λT1:T0 → Type. + λa0,b0:T0. + λe0:a0 = b0. + λso:T1 a0. + eq_rect' ?? (λy,p.T1 y) so ? e0. + *) + +include "logic/equality.ma". + +ndefinition R1 ≝ eq_rect_Type0. + +ndefinition R2 : + ∀T0:Type[0]. + ∀a0:T0. + ∀T1:∀x0:T0. a0=x0 → Type[0]. + ∀a1:T1 a0 (refl ? a0). + ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0]. + ∀b0:T0. + ∀e0:a0 = b0. + ∀b1: T1 b0 e0. + ∀e1:R1 ??? a1 ? e0 = b1. + ∀so:T2 a0 (refl ? a0) a1 (refl ? a1).T2 b0 e0 b1 e1. +#T0;#a0;#T1;#a1;#T2;#b0;#e0;#b1;#e1;#H; +napply (eq_rect_Type0 ????? e1); +napply (R1 ?? ? ?? e0); +napply H; +nqed. + +ndefinition R3 : + ∀T0:Type[0]. + ∀a0:T0. + ∀T1:∀x0:T0. a0=x0 → Type[0]. + ∀a1:T1 a0 (refl ? a0). + ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type[0]. + ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1). + ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1. + ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 x0 p0 ? p1 a2 = x2 → Type[0]. + ∀b0:T0. + ∀e0:a0 = b0. + ∀b1: T1 b0 e0. + ∀e1:R1 ??? a1 ? e0 = b1. + ∀b2: T2 b0 e0 b1 e1. + ∀e2:R2 ???? T2 b0 e0 ? e1 a2 = b2. + ∀so:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).T3 b0 e0 b1 e1 b2 e2. +#T0;#a0;#T1;#a1;#T2;#a2;#T3;#b0;#e0;#b1;#e1;#b2;#e2;#H; +napply (eq_rect_Type0 ????? e2); +napply (R2 ?? ? ??? e0 ? e1); +napply H; +nqed. \ No newline at end of file diff --git a/helm/software/matita/tests/destruct_bb.ma b/helm/software/matita/tests/destruct_bb.ma new file mode 100644 index 000000000..a494909f7 --- /dev/null +++ b/helm/software/matita/tests/destruct_bb.ma @@ -0,0 +1,256 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) +(* +include "nat/nat.ma". +include "list/list.ma". + +inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝ +| il_s : ∀n.T n → index_list T n n +| il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n. + +lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p). + ∀m',n'.S m' = m → S n' = n → index_list T m' n'. +intros 5;elim i +[destruct;apply il_s;apply f;assumption +|apply il_c + [apply f;rewrite > H;assumption + |apply f1 + [rewrite > H;reflexivity + |assumption]]] +qed. + +definition r1 : ∀T0,T1,a0,b0,e0.T1 a0 → T1 b0 ≝ + λT0:Type.λT1:T0 → Type. + λa0,b0:T0. + λe0:a0 = b0. + λso:T1 a0. + eq_rect' ?? (λy,p.T1 y) so ? e0. + *) + +definition R1 ≝ eq_rect'. + + +definition R2 : + ∀T0:Type. + ∀a0:T0. + ∀T1:∀x0:T0. a0=x0 → Type. + ∀a1:T1 a0 (refl_eq ? a0). + ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type. + ∀b0:T0. + ∀e0:a0 = b0. + ∀b1: T1 b0 e0. + ∀e1:R1 ??? a1 ? e0 = b1. + ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1. +intros 8;intros 2 (e1 H); +apply (eq_rect' ????? e1); +apply (R1 ?? ? ?? e0); +simplify;assumption; +qed. + +definition R3 : + ∀T0:Type. + ∀a0:T0. + ∀T1:∀x0:T0. a0=x0 → Type. + ∀a1:T1 a0 (refl_eq ? a0). + ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type. + ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1). + ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1. + ∀x2:T2 x0 p0 x1 p1.R2 ?????? p0 ? p1 a2 = x2→ Type. + ∀b0:T0. + ∀e0:a0 = b0. + ∀b1: T1 b0 e0. + ∀e1:R1 ??? a1 ? e0 = b1. + ∀b2: T2 b0 e0 b1 e1. + ∀e2:R2 ?????? e0 ? e1 a2 = b2. + ∀so:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2. +intros 12;intros 2 (e2 H); +apply (eq_rect' ????? e2); +apply (R2 ?? ? ??? e0 ? e1); +simplify;assumption; +qed. + + + +definition r3 : ∀T0:Type.∀T1:T0 → Type.∀T2:∀t0:T0.∀t1:T1 t0.Type. + ∀T3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type. + ∀a0,b0:T0.∀e0:a0 = b0. + ∀a1:T1 a0.∀b1:T1 b0.∀e1:r1 ?? ?? e0 a1 = b1. + ∀a2:T2 a0 a1.∀b2:T2 b0 b1. + ∀e2: r2 ????? e0 ?? e1 a2 = b2. + T3 a0 a1 a2 → T3 b0 b1 b2. +intros 12;intro e2;intro H; +apply (eq_rect' ????? e2); +apply (R2 ?? ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ? e0 ? e1); +simplify;assumption; +qed. + + +apply (R2 ?? (λy0,p0,y1,p1.T3 y0 y1 (r2 T0 T1 T2 a0 y0 p0 a1 y1 p1 a2)) ??? e0 e1); +simplify; + + + + + + λT0:Type.λT1:T0 → Type.λT2:∀t0:T0.∀t1:T1 t0.Type. + λT3:∀t0:T0.∀t1:T1 t0.∀t2:T2 t0 t1.Type. + + λa0,b0:T0. + λe0:a0 = b0. + + λa1:T1 a0.λb1: T1 b0. + λe1:r1 ???? e0 a1 = b1. + + λa2:T2 a0 a1.λb2: T2 b0 b1. + λe2:r2 ????? e0 ?? e1 a2 = b2. + + λso:T3 a0 a1 a2. + eq_rect' ?? (λy,p.T3 b0 b1 y) + (eq_rect' ?? (λy,p.T3 b0 y (r2 ??? ??e0 ??p a2)) + (eq_rect' T0 a0 (λy.λp:a0 = y.T3 y (r1 ?? a0 y p a1) (r2 ??? ??p a2)) so b0 e0) + ? e1) + ? e2. + +let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝ + match n with + [ O ⇒ Type + | S p ⇒ match l2 with + [ nil ⇒ Type (* dummy *) + | cons T tl ⇒ ∀t:app_type_list l1 T.iter_type p (l1@[t]) tl ]]. + +lemma app_type_list : ∀l:list Type.∀T:iter_type l.Type. +intro; +elim l +[apply i +|simplify in i;apply F;apply i;apply a] +qed. + +definition type_list_cons : ∀l:list Type.iter_type l → list Type ≝ + λl,T.app_type_list l T :: l. + +let rec build_dep_type n T acc ≝ + match n with + [ O ⇒ acc + | S p ⇒ +Type → list Type → Type. + λta,l.match l + +inductive II : nat → Type ≝ +| k1 : ∀n.II n +| k2 : ∀n.II n +| k3 : ∀n,m. II n → II m → II O. + +inductive JJ : nat → Type ≝ +| h1 : JJ O +| h2 : JJ (S O) +| h3 : ∀n,m. JJ n → JJ m → JJ O. + +(* + +lemma test: h3 ?? h1 h2 = h3 ?? h2 h1 → True. +intro; +letin f ≝ (λx.S (S x)); +cut (∃a,b.S a = f b); +[decompose;cut (S (S a) = S (f a1)) + [|clear H;destruct; +cut (∀→ True) +[elim Hcut; +qed. +*) + +definition IId : ∀n,m.II m → II n → Type ≝ + λa,b,x,y.match x with + [ k1 n ⇒ match y with + [ k1 n' ⇒ ∀P:Type.(n = n' → P) → P + | k2 n' ⇒ ∀P:Type.P + | k3 m n p' q' ⇒ ∀P:Type.P ] + | k2 n ⇒ match y with + [ k1 n' ⇒ ∀P:Type.P + | k2 n' ⇒ ∀P:Type.(n = n' → P) → P + | k3 m' n' p' q' ⇒ ∀P:Type.P ] + | k3 m n p q ⇒ match y with + [ k1 n' ⇒ ∀P:Type.P + | k2 n' ⇒ ∀P:Type.P + | k3 m' n' p' q' ⇒ ∀P:Type.(∀e1:m = m'.∀e2:n = n'. (eq_rect ??? p ? e1) = p' + → (eq_rect ??? q ? e2) = q' → P) → P ]]. + +lemma IInc : ∀n,x,y.x = y → IId n n x y. +intros;rewrite > H;elim y;simplify;intros; +[apply f;reflexivity +|apply f;reflexivity +|apply f;reflexivity] +qed. + +inductive I1 : nat → Type ≝ +| kI1 : ∀n.I1 n. + +inductive I2 : ∀n:nat.I1 n → Type ≝ +| kI2 : ∀n,i.I2 n i. + +inductive I3 : Type ≝ +| kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3. + +definition I3d: I3 → I3 → Type ≝ +λx,y.match x with +[ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with + [ kI3 u1 u2 u3 ⇒ ∀P:Type. + (∀e1: t1 = u1. + ∀e2: (eq_rect ?? (λx.I1 x) t2 ? e1) = u2. + ∀e3: (eq_rect' ?? (λy,p.I2 u1 y) + (eq_rect' ?? (λy,p.I2 y (eq_rect ?? (λx.I1 x) t2 ? p)) t3 ? e1) + ? e2) = u3.P) → P]]. + +lemma I3nc : ∀a,b.a = b → I3d a b. +intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity; +qed. + +definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝ + λa,b,c,d,x,y.match x with + [ c1 n ⇒ match y with + [ c1 n' ⇒ ∀P:Type.(n = n' → P) → P + | c2 n' ⇒ ∀P:Type.P + | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ] + | c2 n ⇒ match y with + [ c1 n' ⇒ ∀P:Type.P + | c2 n' ⇒ ∀P:Type.(n = n' → P) → P + | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ] + | c3 m n p q h i ⇒ match y with + [ c1 n' ⇒ ∀P:Type.P + | c2 n' ⇒ ∀P:Type.P + | c3 m' n' p' q' h' i' ⇒ + ∀P:Type.(∀e1:m = m'.∀e2:n = n'. ∀e3:p = p'. ∀e4:q = q'. + (eq_rect ?? (λm.KK m n') (eq_rect ?? (λn.KK m n) h n' e2) m' e1) = h' + → (eq_rect ?? (λp.KK p q') (eq_rect ?? (λq.KK p q) i ? e4) ? e3) = i' → P) → P ]]. + +lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f. +intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity; +qed. + +lemma IIconflict: ∀c,d. + k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False. +intros;apply (IInc ??? H);clear H;intro; +apply (eq_rec ????? e1); +intro;generalize in match e1;elim +apply (eq_rect' ?? (λx.λp.∀e2:x=c.eq_rect ℕ c II (k1 c) x p=k2 x→eq_rect nat x II (k2 x) c e2 = k1 c → False) ?? e1); +simplify;intro; +apply (eq_rect' nat ? (λx.λp:c=x.k1 x = k2 x → eq_rect nat c II (k2 c) x p = k1 x → False) ?? e2); +simplify;intro; + +generalize in match H1; +apply (eq_rect' ?? (λx.λp.eq_rect ℕ c II (k1 c) x p=k2 x→False) ?? e1); +simplify;intro;destruct; +qed. + +elim e1 in H1; + -- 2.39.2