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 *)
33 | generalize in match Hcut.
34 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H);
35 [ intro. rewrite < H1. clear Hcut.
36 | simplify. intros. discriminate H3.
42 (* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
43 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
44 theorem test_inversion2: \forall n. le n O \to n=O.
46 (* inversion begins *)
47 generalize in match (refl_equal nat O).
48 apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H);
49 [ intro. rewrite < H1.
50 | simplify. intros. discriminate H3.