(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/decl".
+
include "nat/times.ma".
include "nat/orders.ma".
assume m: nat.
(* base case *)
by (refl_eq ? O) we proved (O = O) (trivial).
- by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2).
- by (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case).
+ by or_introl we proved (O = O ∨ m = O) (trivial2).
+ using (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case).
(* inductive case *)
we need to prove
(∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
assume n1: nat.
suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
(* base case *)
- by (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2).
- by (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+ by or_intror we proved (S n1 = O ∨ O = O) (pre_base_case2).
+ using (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
(* inductive case *)
we need to prove
(∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
suppose (S n1 * S m1 = O) (absurd_hyp).
simplify in absurd_hyp.
- by (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp').
- by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
+ by sym_eq we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+ by not_eq_O_S we proved False (the_absurd).
by (False_ind ? the_absurd)
done.
(* the induction *)
- by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
done.
(* the induction *)
- by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+ using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
done.
qed.
assume n: nat.
assume m: nat.
(* base case *)
- by _ we proved (O = O) (trivial).
- by _ we proved (O = O ∨ m = O) (trivial2).
- by _ we proved (O*m=O → O=O ∨ m=O) (base_case).
+ we proved (O = O) (trivial).
+ we proved (O = O ∨ m = O) (trivial2).
+ we proved (O*m=O → O=O ∨ m=O) (base_case).
(* inductive case *)
we need to prove
(∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O)
assume n1: nat.
suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp).
(* base case *)
- by _ we proved (S n1 = O ∨ O = O) (pre_base_case2).
- by _ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
+ we proved (S n1 = O ∨ O = O) (pre_base_case2).
+ we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2).
(* inductive case *)
we need to prove
(∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) →
suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless).
suppose (S n1 * S m1 = O) (absurd_hyp).
simplify in absurd_hyp.
- by _ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
- (* BUG: automation failure *)
- by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd).
- (* BUG: automation failure *)
- by (False_ind ? the_absurd)
- done.
+ we proved (O = S (m1+n1*S m1)) (absurd_hyp').
+ we proved False (the_absurd).
+ we proceed by cases on the_absurd to prove (S n1=O ∨ S m1=O).
(* the induction *)
- by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
+ using (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m)
done.
(* the induction *)
- by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
+ using (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n)
done.
qed.
assume P: Prop.
suppose (P ∧ ∃m:nat.m ≠ m) (H).
by H we have P (H1) and (∃x:nat.x≠x) (H2).
- (*BUG:
by H2 let q:nat such that (q ≠ q) (Ineq).
- *)
- (* the next line is wrong, but for the moment it does the job *)
- by H2 let q:nat such that False (Ineq).
by I done.
qed.
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-conclude (S n) = (S m) by (eq_f ? ? ? ? ? H).
+conclude (S n) = (S m) by H.
= (S p) by K.
- = n by (sym_eq ? ? ? L)
+ = n by L
done.
qed.
suppose (n=m) (H).
suppose (S m = S p) (K).
suppose (n = S p) (L).
-conclude (S n) = (S m) by _.
- = (S p) by _.
- = n by _
+conclude (S n) = (S m).
+ = (S p).
+ = n
done.
qed.
we proceed by induction on n to prove False.
case O.
the thesis becomes (O*O=O).
- by (refl_eq ? O) done.
+ done.
case S (m:nat).
by induction hypothesis we know (m*O=O) (I).
the thesis becomes (S m * O = O).