matita/tests/metasenv_ordering.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/metasenv_ordering".
  16
  17 include "legacy/coq.ma".
  18
  19 alias num (instance 0) = "natural number".
  20 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  21
  22 (* REWRITE *)
  23
  24 theorem th1 :
  25    \forall P:Prop.
  26    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  27    1 = 1 \land 1 = 0 \land 2 = 2.
  28    intros. split; split;
  29    [ reflexivity
  30    | rewrite > H;
  31      [ reflexivity | exact nat | exact (0=0) | exact Type ]
  32    ]
  33 qed.
  34
  35 theorem th2 :
  36    \forall P:Prop.
  37    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  38    1 = 1 \land 1 = 0 \land 3 = 3.
  39    intros. split. split.
  40    focus 13.
  41      rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type].
  42    unfocus.
  43    reflexivity.
  44    reflexivity.
  45 qed.
  46
  47 theorem th3 :
  48    \forall P:Prop.
  49    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  50    1 = 1 \land 1 = 0 \land 4 = 4.
  51    intros. split. split.
  52    focus 13.
  53      rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
  54    unfocus.
  55    reflexivity.
  56    reflexivity.
  57 qed.
  58
  59 theorem th4 :
  60    \forall P:Prop.
  61    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  62    1 = 1 \land 1 = 0 \land 5 = 5.
  63    intros. split. split.
  64    focus 13.
  65      rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
  66    unfocus.
  67    reflexivity.
  68    reflexivity.
  69 qed.
  70
  71 (* APPLY *)
  72
  73 theorem th5 :
  74    \forall P:Prop.
  75    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  76    1 = 1 \land 1 = 0 \land 6 = 6.
  77    intros. split. split.
  78    focus 13.
  79      apply H; [exact nat | exact (0=0) | exact Type].
  80    unfocus.
  81    reflexivity.
  82    reflexivity.
  83 qed.
  84
  85 theorem th6 :
  86    \forall P:Prop.
  87    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  88    1 = 1 \land 1 = 0 \land 7 = 7.
  89    intros. split. split.
  90    focus 13.
  91      apply (H ?); [exact nat | exact (0=0) | exact Type].
  92    unfocus.
  93    reflexivity.
  94    reflexivity.
  95 qed.
  96
  97 theorem th7 :
  98    \forall P:Prop.
  99    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
 100    1 = 1 \land 1 = 0 \land 8 = 8.
 101    intros. split. split.
 102    focus 13.
 103      apply (H ? ?); [exact nat | exact (0=0) | exact Type].
 104    unfocus.
 105    reflexivity.
 106    reflexivity.
 107 qed.
 108
 109 theorem th8 :
 110    \forall P:Prop.
 111    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
 112    1 = 1 \land 1 = 0 \land 9 = 9.
 113    intros. split. split.
 114    focus 13.
 115      apply (H ? ? ?); [exact nat | exact (0=0) | exact Type].
 116    unfocus.
 117    reflexivity.
 118    reflexivity.
 119 qed.
 120
 121 (* ELIM *)
 122
 123 theorem th9:
 124   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
 125   intros (P Q R S r s H).
 126   elim (H ? ?); [split; assumption | exact r | exact s].
 127   qed.
 128
 129 theorem th10:
 130   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
 131   intros (P Q R S r s H).
 132   elim (H ?); [split; assumption | exact r | exact s].
 133   qed.
 134
 135 theorem th11:
 136   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
 137   intros (P Q R S r s H).
 138   elim H; [split; assumption | exact r | exact s].
 139   qed.