helm/software/matita/tests/inversion.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/tests/inversion_sum/".
  16 include "../legacy/coq.ma".
  17
  18
  19 alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
  20 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
  21
  22 inductive sum (n:nat) : nat \to nat \to Set \def
  23   k: \forall x,y. n = x + y \to sum n x y.
  24
  25
  26
  27
  28 theorem t: \forall x,y. \forall H: sum x y O.
  29           match H with [ (k a b p) \Rightarrow a ] = x.
  30  intros.
  31  inversion H.
  32
  33  (*
  34  cut (y = y \to O = O \to match H with [ (k a b p) \Rightarrow a] = x).
  35  apply Hcut; reflexivity.
  36  apply
  37   (sum_ind ?
  38     (\lambda a,b,K. y=a \to O=b \to
  39         match K with [ (k a b p) \Rightarrow a ] = x)
  40      ? ? ? H).
  41  goal 16.*)
  42  simplify. intros.
  43  generalize in match H1.
  44  rewrite < H2; rewrite < H3.intro.
  45  rewrite > H4.auto new library.
  46 qed.
  47
  48 theorem t1: \forall x,y. sum x y O \to x = y.
  49 intros.
  50
  51 (*
  52 cut y=y \to O=O \to x = y.
  53 apply Hcut.reflexivity. reflexivity.
  54 apply (sum_ind ? (\lambda a,b,K. y=a \to O=b \to x=a) ? ? ? s).*)
  55
  56 (*apply (sum_ind ? (\lambda a,b,K. y = a \to O = b \to  x = a) ? ? ? s).*)
  57 inversion s.
  58 intros.simplify.
  59 intros.
  60 rewrite > H. rewrite < H2.  auto new library.
  61 qed.