1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/test/coercions_propagation/".
17 include "logic/connectives.ma".
18 include "nat/orders.ma".
19 alias num (instance 0) = "natural number".
21 inductive sigma (A:Type) (P:A → Prop) : Type ≝
22 sigma_intro: ∀a:A. P a → sigma A P.
24 interpretation "sigma" 'exists \eta.x =
25 (cic:/matita/test/coercions_propagation/sigma.ind#xpointer(1/1) _ x).
27 definition inject ≝ λP.λa:nat.λp:P a. sigma_intro ? P ? p.
29 coercion cic:/matita/test/coercions_propagation/inject.con 0 1.
31 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ sigma_intro w _ ⇒ w].
33 coercion cic:/matita/test/coercions_propagation/eject.con.
35 alias num (instance 0) = "natural number".
37 theorem test: ∃n. 0 ≤ n.
38 apply (S O : ∃n. 0 ≤ n).
42 theorem test2: nat → ∃n. 0 ≤ n.
43 apply ((λn:nat. 0) : nat → ∃n. 0 ≤ n);
47 theorem test3: (∃n. 0 ≤ n) → nat.
48 apply ((λn:nat.n) : (∃n. 0 ≤ n) → nat).
51 theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
52 apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
57 theorem test5: nat → ∃n. 1 ≤ n.
67 [ cases (aux name_con); simplify; ] autobatch;
70 inductive NN (A:Type) : nat -> Type ≝
72 | NS : ∀n:nat. NN A n → NN A (S n).
74 definition injectN ≝ λA,k.λP.λa:NN A k.λp:P a. sigma_intro ? P ? p.
76 coercion cic:/matita/test/coercions_propagation/injectN.con 0 1.
78 definition ejectN ≝ λA,k.λP.λc: ∃n:NN A k.P n. match c with [ sigma_intro w _ ⇒ w].
80 coercion cic:/matita/test/coercions_propagation/ejectN.con.
83 λA,k.λx:NN A k. 1 <= k.
85 theorem test51_byhand: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
88 let rec aux (w : nat) (n : NN A w) on n : ∃p:NN A (S w).PN ? ? p ≝
89 match n in NN return λx.λm:NN A x.∃p:NN A (S x).PN ? ? p with
90 [ NO ⇒ injectN ? ? ? (NS A ? (NO A)) ?
91 | NS x m ⇒ injectN ? ? ? (NS A (S x) (ejectN ? ? ? (aux ? m))) ?
95 : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
96 [2: cases (aux x m); simplify; autobatch ] unfold PN; autobatch;
99 theorem f : nat -> nat -> ∃n:nat.O <= n.
100 apply (λx,y:nat.y : nat -> nat -> ∃n:nat. O <= n).
104 axiom F : nat -> nat -> nat.
106 theorem f1 : nat -> nat -> ∃n:nat.O <= n.
107 apply (F : nat -> nat -> ∃n:nat. O <= n).
111 theorem test51: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
113 (* MANCA UN LIFT forse NEL FIX *)
115 let rec aux (w : nat) (n : NN A w) on n : NN A (S w) ≝
116 match n in NN return λx.λm:NN A x.NN A (S x) with
118 | NS x m ⇒ NS A (S x) (aux ? m)
122 : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
123 [ cases (aux name_con); simplify; ] autobatch;
126 (* guarded troppo debole
127 theorem test5: nat → ∃n. 1 ≤ n.
129 let rec aux n : nat ≝
148 theorem test5: nat → ∃n. 1 ≤ n.
150 let rec aux (n : nat) : ∃n. 1 ≤ n ≝
152 [ O => (S O : ∃n. 1 ≤ n)
153 | S m => (S (aux m) : ∃n. 1 ≤ n)
155 inject ? (S (eject ? (aux m))) ? *)
167 Re1: nat => nat |- body[Rel1] : nat => nat
168 Re1: nat => X |- body[Rel1] : nat => nat : nat => X
169 Re1: Y => X |- body[Rel1] : nat => nat : Y => X
174 theorem test5: (∃n. 2 ≤ n) → ∃n. 1 ≤ n.
177 let rec aux n : eject ? n = eject ? k → ∃n. 1 ≤ n ≝
178 match eject ? n return λx:nat. x = eject ? k → ∃n. 1 ≤ n with
179 [ O ⇒ λH: 0 = eject ? k.
181 | S m ⇒ λH: S m = eject ? k.
182 sigma_intro ? ? (S m) ?
185 aux k (refl_eq ? (eject ? k)));
190 generalize in match H; clear H;
192 [ apply (sigma_intro ? ? 0);
193 | apply (sigma_intro ? ? (S n));
198 let rec aux n : ∃n. 1 ≤ n ≝
202 | S m ⇒ S (eject ? (aux m))
208 let rec aux n : nat ≝
215 : (∃n. 2 ≤ n) → ∃n. 1 ≤ n);
220 theorem test5: nat → ∃n. 0 ≤ n.
223 (match n return λ_.∃n.0 ≤ n with [O ⇒ (0 : ∃n.0 ≤ n) | S n' ⇒ ex_intro ? ? n' ?]