]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/tests/coercions_propagation.ma
restructuring
[helm.git] / matita / matita / tests / coercions_propagation.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16
17 include "logic/connectives.ma".
18 include "nat/orders.ma".
19
20 inductive sigma (A:Type) (P:A → Prop) : Type ≝
21  sigma_intro: ∀a:A. P a → sigma A P.
22
23 interpretation "sigma" 'exists \eta.x =
24   (cic:/matita/tests/coercions_propagation/sigma.ind#xpointer(1/1) _ x).
25   
26 definition inject ≝ λP.λa:nat.λp:P a. sigma_intro ? P ? p.
27
28 coercion cic:/matita/tests/coercions_propagation/inject.con 0 1.
29
30 definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ sigma_intro w _ ⇒ w].
31
32 coercion cic:/matita/tests/coercions_propagation/eject.con.
33
34 alias num (instance 0) = "natural number".
35 theorem test: ∃n. 0 ≤ n.
36  apply (S O : ∃n. 0 ≤ n).
37  autobatch.
38 qed.
39
40 theorem test2: nat → ∃n. 0 ≤ n.
41  apply ((λn:nat. 0) : nat → ∃n. 0 ≤ n);
42  autobatch.
43 qed.
44
45 theorem test3: (∃n. 0 ≤ n) → nat.
46  apply ((λn:nat.n) : (∃n. 0 ≤ n) → nat).
47 qed.
48
49 theorem test4: (∃n. 1 ≤ n) → ∃n. 0 < n.
50  apply ((λn:nat.n) : (∃n. 1 ≤ n) → ∃n. 0 < n);
51  cases s;
52  assumption.
53 qed.
54
55 theorem test5: nat → ∃n. 1 ≤ n.
56 apply (
57  let rec aux n : nat ≝
58   match n with
59    [ O ⇒ 1
60    | S m ⇒ S (aux m)
61    ]
62  in
63   aux
64 : nat → ∃n. 1 ≤ n);
65 [ cases (aux n1); simplify; ] autobatch;
66 qed.
67
68 inductive NN (A:Type) : nat -> Type ≝
69  | NO : NN A O
70  | NS : ∀n:nat. NN A n → NN A (S n).
71  
72 definition injectN ≝ λA,k.λP.λa:NN A k.λp:P a. sigma_intro ? P ? p.
73
74 coercion cic:/matita/tests/coercions_propagation/injectN.con 0 1.
75
76 definition ejectN ≝ λA,k.λP.λc: ∃n:NN A k.P n. match c with [ sigma_intro w _ ⇒ w].
77
78 coercion cic:/matita/tests/coercions_propagation/ejectN.con.
79
80 definition PN :=
81  λA,k.λx:NN A k. 1 <= k.
82
83 theorem test51_byhand: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
84 intros 1;
85 apply (
86  let rec aux (w : nat) (n : NN A w) on n : ∃p:NN A (S w).PN ? ? p ≝
87   match n in NN return λx.λm:NN A x.∃p:NN A (S x).PN ? ? p with
88    [ NO ⇒ injectN ? ? ? (NS A ? (NO A)) ?
89    | NS x m ⇒ injectN ? ? ? (NS A (S x) (ejectN ? ? ? (aux ? m))) ?  
90    ]
91  in
92   aux
93 : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m);
94 [2: cases (aux x m); simplify; autobatch ] unfold PN; autobatch;
95 qed.
96
97 theorem f : nat -> nat -> ∃n:nat.O <= n.
98 apply (λx,y:nat.y : nat -> nat -> ∃n:nat. O <= n).
99 apply le_O_n; 
100 qed.
101
102 axiom F : nat -> nat -> nat.
103
104 theorem f1 : nat -> nat -> ∃n:nat.O <= n.
105 apply (F : nat -> nat -> ∃n:nat. O <= n).
106 apply le_O_n; 
107 qed.
108
109 theorem test51: ∀A,k. NN A k → ∃n:NN A (S k). PN ? ? n.
110 intros 1;
111 letin xxx ≝ (
112  let rec aux (w : nat) (n : NN A w) on n : NN A (S w) ≝
113   match n in NN return λx.λm:NN A x.NN A (S x) with
114    [ NO ⇒ NS A ? (NO A)
115    | NS x m ⇒ NS A (S x) (aux ? m)  
116    ]
117  in
118   aux
119 : ∀n:nat. NN A n → ∃m:NN A (S n). PN ? ? m); [3: apply xxx];
120 unfold PN in aux ⊢ %; [cases (aux n2 n3)] autobatch;
121 qed.
122
123 (* guarded troppo debole *)
124 theorem test522: nat → ∃n. 1 ≤ n.
125 apply (
126  let rec aux n : nat ≝
127   match n with
128    [ O ⇒ 1
129    | S m ⇒ S (aux m)
130    ]
131  in
132   aux
133 : nat → ∃n. 1 ≤ n);
134 [ cases (aux n1); simplify;
135   autobatch
136 | autobatch].
137 qed.
138