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  (* inversion begins *)
  16  cut O=O.
  17   (* goal 2: 0 = 0 *)
  18   goal 7. reflexivity.
  19   (* goal 1 *)
  20   generalize in match Hcut.
  21   apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  22   (* first goal (left open) *)
  23   intro. rewrite < H1.
  24   clear Hcut.
  25   (* second goal (closed) *)
  26   goal 14.
  27   simplify. intros.
  28   discriminate H3.
  29   (* inversion ends *)
  30   reflexivity.
  31 qed.
  32
  33 (* Piu' semplice e non lascia l'ipotesi inutile Hcut *)
  34 alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)".
  35 theorem test_inversion2: \forall n. le n O \to n=O.
  36  intros.
  37  (* inversion begins *)
  38  generalize in match (refl_equal nat O).
  39  apply (le_ind ? (\lambda x. O=x \to n=x) ? ? ? H).
  40  (* first goal (left open) *)
  41  intro. rewrite < H1.
  42  (* second goal (closed) *)
  43  goal 13.
  44  simplify. intros.
  45  discriminate H3.
  46  (* inversion ends *)
  47  reflexivity.
  48 qed.