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/tests/inversion/".
18 inductive nat : Set \def
22 inductive le (n:nat) : nat \to Prop \def
24 | leS : \forall m. le n m \to le n (S m).
26 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
28 theorem test_inversion: \forall n. le n O \to n=O.
30 (* inversion begins *)
35 generalize in match Hcut.
36 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
37 (* first goal (left open) *)
40 (* second goal (closed) *)
48 (* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
49 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
50 theorem test_inversion2: \forall n. le n O \to n=O.
52 (* inversion begins *)
53 generalize in match (refl_equal nat O).
54 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
55 (* first goal (left open) *)
57 (* second goal (closed) *)