]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/tests/decl.ma
better test for church numerals
[helm.git] / helm / software / matita / tests / decl.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 set "baseuri" "cic:/matita/tests/decl".
16
17 include "nat/times.ma".
18 include "nat/orders.ma".
19
20 theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
21  assume n: nat.
22  assume m: nat.
23  (* base case *)
24  by (refl_eq ? O) we proved (O = O) (trivial).
25  by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2).
26  by (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case).
27  (* inductive case *)
28  we need to prove
29   (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
30   (inductive_case).
31    assume n1: nat.
32    suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
33    (* base case *)
34    by (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2).
35    by (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
36    (* inductive case *)
37    we need to prove
38     (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
39       (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
40      assume m1: nat.
41      suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
42      suppose (S n1 * S m1 = O) (absurd_hyp).
43      simplify in absurd_hyp.
44      by (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp').
45      by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
46      by (False_ind ? the_absurd)
47    done.
48    (* the induction *)
49    by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
50  done.
51  (* the induction *)
52  by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
53 done.
54 qed.
55  
56 theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
57  intros 2.
58  elim n 0
59   [ intro;
60     left;
61     reflexivity
62   | intro;
63     elim m 0
64     [ intros;
65       right;
66       reflexivity
67     | intros;
68       simplify in H2;
69       lapply (sym_eq ? ? ? H2);
70       elim (not_eq_O_S ? Hletin)
71     ]
72   ]
73 qed.
74
75 theorem easy15: ∀n,m. n * m = O → n = O ∨ m = O.
76  assume n: nat.
77  assume m: nat.
78  (* base case *)
79  by _ we proved (O = O) (trivial).
80  by _ we proved (O = O ∨ m = O) (trivial2).
81  by _ we proved (O*m=O → O=O ∨ m=O) (base_case).
82  (* inductive case *)
83  we need to prove
84   (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
85   (inductive_case).
86    assume n1: nat.
87    suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
88    (* base case *)
89    by _ we proved (S n1 = O ∨ O = O) (pre_base_case2).
90    by _ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
91    (* inductive case *)
92    we need to prove
93     (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
94       (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2).
95      assume m1: nat.
96      suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
97      suppose (S n1 * S m1 = O) (absurd_hyp).
98      simplify in absurd_hyp.
99      by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
100      (* BUG: automation failure *)
101      by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
102      (* BUG: automation failure *)
103      by (False_ind ? the_absurd)
104    done.
105    (* the induction *)
106    by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
107  done.
108  (* the induction *)
109  by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
110 done.
111 qed.
112
113 theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
114  assume P: Prop.
115  suppose (P ∧ ∃m:nat.m ≠ m) (H).
116  by H we have P (H1) and (∃x:nat.x≠x) (H2).
117  (*BUG:
118  by H2 let q:nat such that (q ≠ q) (Ineq).
119  *)
120  (* the next line is wrong, but for the moment it does the job *)
121  by H2 let q:nat such that False (Ineq).
122  by I done.
123 qed.
124
125 theorem easy4: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
126 assume n: nat.
127 assume m:nat.
128 assume p:nat.
129 suppose (n=m) (H).
130 suppose (S m = S p) (K).
131 suppose (n = S p) (L).
132 conclude (S n) = (S m) by (eq_f ? ? ? ? ? H).
133              = (S p) by K.
134              = n by (sym_eq ? ? ? L)
135 done.
136 qed.
137
138 theorem easy45: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
139 assume n: nat.
140 assume m:nat.
141 assume p:nat.
142 suppose (n=m) (H).
143 suppose (S m = S p) (K).
144 suppose (n = S p) (L).
145 conclude (S n) = (S m) by _.
146              = (S p) by _.
147              = n by _
148 done.
149 qed.
150
151 theorem easy5: ∀n:nat. n*O=O.
152 assume n: nat.
153 (* Bug here: False should be n*0=0 *)
154 we proceed by induction on n to prove False. 
155  case O.
156    the thesis becomes (O*O=O).
157    by (refl_eq ? O) done.
158  case S (m:nat).
159   by induction hypothesis we know (m*O=O) (I).
160   the thesis becomes (S m * O = O).
161   (* Bug here: missing that is equivalent to *)
162   simplify.
163   by I done.
164 qed.
165
166 inductive tree : Type ≝
167    Empty: tree
168  | Node: tree → tree → tree.
169  
170 let rec size t ≝
171  match t with
172   [ Empty ⇒ O
173   | (Node t1 t2) ⇒ S ((size t1) + (size t2))
174   ].
175   
176 theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty. 
177  assume t: tree.
178  suppose (O ≮ O) (trivial).
179  (*Bug here: False should be something else *)
180  we proceed by induction on t to prove False.
181   case Empty.
182     the thesis becomes (O < size Empty → Empty ≠ Empty).
183      suppose (O < size Empty) (absurd)
184      that is equivalent to (O < O).
185      (* Here the "natural" language is not natural at all *)
186      we proceed by induction on (trivial absurd) to prove False.
187   (*Bug here: this is what we want
188   case Node (t1:tree) (t2:tree).
189      by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
190      by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2). *)
191   (*This is the best we can do right now*)
192   case Node.
193    assume t1: tree.
194    by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
195    assume t2: tree.
196    by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2).
197    suppose (O < size (Node t1 t2)) (useless).
198    we need to prove (Node t1 t2 ≠ Empty) (final)
199    or equivalently (Node t1 t2 = Empty → False).
200      suppose (Node t1 t2 = Empty) (absurd).
201      (* Discriminate should really generate a theorem to be useful with
202         declarative tactics *)
203      destruct absurd.
204      by final
205    done.
206 qed.