helm/matita/tests/inversion.ma

   1 inductive nat : Set \def
   2    O : nat
   3  | S : nat \to nat.
   4
   5 inductive le (n:nat) : nat \to Prop \def
   6    leO : le n n
   7  | leS : \forall m. le n m \to le n (S m).
   8
   9 alias symbol "eq" (instance 0) = "leibnitz's equality".
  10
  11 theorem test_inversion: \forall n. le n O \to n=O.
  12  intros.
  13  (* inversion begins *)
  14  cut O=O.
  15   (* goal 2: 0 = 0 *)
  16   goal 7. reflexivity.
  17   (* goal 1 *)
  18   generalize Hcut.
  19   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  20   (* first goal (left open) *)
  21   intro. rewrite right H1.
  22   clear Hcut.
  23   (* second goal (closed) *)
  24   goal 14.
  25   simplify. intros.
  26   discriminate H3.
  27   (* inversion ends *)
  28   reflexivity.
  29 qed.
  30
  31 (* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
  32 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
  33 theorem test_inversion2: \forall n. le n O \to n=O.
  34  intros.
  35  (* inversion begins *)
  36  generalize (refl_equal nat O).
  37  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  38  (* first goal (left open) *)
  39  intro. rewrite right H1.
  40  (* second goal (closed) *)
  41  goal 13.
  42  simplify. intros.
  43  discriminate H3.
  44  (* inversion ends *)
  45  reflexivity.
  46 qed.