1. Tactic generalize ported to patterns and activated in matita.

[helm.git] / helm / matita / tests / inversion.ma

diff --git a/helm/matita/tests/inversion.ma b/helm/matita/tests/inversion.ma
new file mode 100644 (file)
index 0000000..ccbc4d9
--- /dev/null
+++ b/helm/matita/tests/inversion.ma
@@ -0,0 +1,22 @@
+inductive nat : Set \def
+   O : nat
+ | S : nat \to nat.
+ 
+inductive le (n:nat) : nat \to Prop \def
+   leO : le n n
+ | leS : \forall m. le n m \to le n (S m).
+
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+
+theorem test_inversion: \forall n. le n O \to n=O.
+ intros.
+ cut O=O.
+  (* goal 2: 0 = 0 *)
+  goal 7. reflexivity.
+  (* goal 1 *)
+  generalize Hcut.      (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
+  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
+  intro. reflexivity.
+  simplify. intros.
+  (* manca discriminate H3 *)
+qed.
\ No newline at end of file