helm/matita/tests/inversion.ma

   1 set "baseuri" "cic:/matita/tests/".
   2
   3 inductive nat : Set \def
   4    O : nat
   5  | S : nat \to nat.
   6
   7 inductive le (n:nat) : nat \to Prop \def
   8    leO : le n n
   9  | leS : \forall m. le n m \to le n (S m).
  10
  11 alias symbol "eq" (instance 0) = "leibnitz's equality".
  12
  13 theorem test_inversion: \forall n. le n O \to n=O.
  14  intros.
  15  cut O=O.
  16   (* goal 2: 0 = 0 *)
  17   goal 7. reflexivity.
  18   (* goal 1 *)
  19   generalize Hcut.      (* non attaccata. Dovrebbe dare 0=0 -> n=0 *)
  20   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  21   intro. reflexivity.
  22   simplify. intros.
  23   discriminate H3.
  24 qed.
  25
  26 (* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
  27 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
  28 theorem test_inversion2: \forall n. le n O \to n=O.
  29  intros.
  30  generalize (refl_equal nat O).
  31  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  32  intro. reflexivity.
  33  simplify. intros.
  34  discriminate H3.
  35 qed.