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/decl".
17 include "nat/times.ma".
18 include "nat/orders.ma".
20 theorem easy: ∀n,m. n * m = O → n = O ∨ m = O.
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).
29 (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
32 suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
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).
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).
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)
49 by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
52 by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
56 theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O.
69 lapply (sym_eq ? ? ? H2);
70 elim (not_eq_O_S ? Hletin)
76 theorem easy3: ∀A:Prop. (A ∧ ∃n:nat.n ≠ n) → True.
78 suppose (P ∧ ∃m:nat.m ≠ m) (H).
79 by H we have P (H1) and (∃x:nat.x≠x) (H2).
81 by H2 let q:nat such that (q ≠ q) (Ineq).
83 (* the next line is wrong, but for the moment it does the job *)
84 by H2 let q:nat such that False (Ineq).
88 theorem easy4: ∀n,m,p. n = m → S m = S p → n = S p → S n = n.
93 suppose (S m = S p) (K).
94 suppose (n = S p) (L).
95 obtain (S n) = (S m) by (eq_f ? ? ? ? ? H).
97 = n by (sym_eq ? ? ? L)
101 theorem easy5: ∀n:nat. n*O=O.
103 (* Bug here: False should be n*0=0 *)
104 we proceed by induction on n to prove False.
106 the thesis becomes (O*O=O).
107 by (refl_eq ? O) done.
109 by induction hypothesis we know (m*O=O) (I).
110 the thesis becomes (S m * O = O).
111 (* Bug here: missing that is equivalent to *)
116 inductive tree : Type ≝
118 | Node: tree → tree → tree.
123 | (Node t1 t2) ⇒ S ((size t1) + (size t2))
126 theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
128 suppose (O ≮ O) (trivial).
129 (*Bug here: False should be something else *)
130 we proceed by induction on t to prove False.
132 the thesis becomes (O < size Empty → Empty ≠ Empty).
133 suppose (O < size Empty) (absurd)
134 that is equivalent to (O < O).
135 (* Here the "natural" language is not natural at all *)
136 we proceed by induction on (trivial absurd) to prove False.
137 (*Bug here: this is what we want
138 case Node (t1:tree) (t2:tree).
139 by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
140 by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2). *)
141 (*This is the best we can do right now*)
144 by induction hypothesis we know (O < size t1 → t1 ≠ Empty) (Ht1).
146 by induction hypothesis we know (O < size t2 → t2 ≠ Empty) (Ht2).
147 suppose (O < size (Node t1 t2)) (useless).
148 we need to prove (Node t1 t2 ≠ Empty) (final)
149 or equivalently (Node t1 t2 = Empty → False).
150 suppose (Node t1 t2 = Empty) (absurd).
151 (* Discriminate should really generate a theorem to be useful with
152 declarative tactics *)