helm/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 "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    goal 13.
  30    rewrite > H; [reflexivity | exact nat | exact 0=0 | exact Type].
  31    reflexivity.
  32    reflexivity.
  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    goal 13.
  41    rewrite > H ?; [reflexivity | exact nat | exact 0=0 | exact Type].
  42    reflexivity.
  43    reflexivity.
  44 qed.
  45
  46 theorem th3 :
  47    \forall P:Prop.
  48    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  49    1 = 1 \land 1 = 0 \land 4 = 4.
  50    intros. split. split.
  51    goal 13.
  52    rewrite > H ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
  53    reflexivity.
  54    reflexivity.
  55 qed.
  56
  57 theorem th4 :
  58    \forall P:Prop.
  59    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  60    1 = 1 \land 1 = 0 \land 5 = 5.
  61    intros. split. split.
  62    goal 13.
  63    rewrite > H ? ? ?; [reflexivity | exact nat | exact 0=0 | exact Type].
  64    reflexivity.
  65    reflexivity.
  66 qed.
  67
  68 (* APPLY *)
  69
  70 theorem th5 :
  71    \forall P:Prop.
  72    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  73    1 = 1 \land 1 = 0 \land 6 = 6.
  74    intros. split. split.
  75    goal 13.
  76    apply H; [exact nat | exact 0=0 | exact Type].
  77    reflexivity.
  78    reflexivity.
  79 qed.
  80
  81 theorem th6 :
  82    \forall P:Prop.
  83    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  84    1 = 1 \land 1 = 0 \land 7 = 7.
  85    intros. split. split.
  86    goal 13.
  87    apply H ?; [exact nat | exact 0=0 | exact Type].
  88    reflexivity.
  89    reflexivity.
  90 qed.
  91
  92 theorem th7 :
  93    \forall P:Prop.
  94    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
  95    1 = 1 \land 1 = 0 \land 8 = 8.
  96    intros. split. split.
  97    goal 13.
  98    apply H ? ?; [exact nat | exact 0=0 | exact Type].
  99    reflexivity.
 100    reflexivity.
 101 qed.
 102
 103 theorem th8 :
 104    \forall P:Prop.
 105    \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0).
 106    1 = 1 \land 1 = 0 \land 9 = 9.
 107    intros. split. split.
 108    goal 13.
 109    apply H ? ? ?; [exact nat | exact 0=0 | exact Type].
 110    reflexivity.
 111    reflexivity.
 112 qed.
 113
 114 (* ELIM *)
 115
 116 theorem th9:
 117   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
 118   intros [P; Q; R; S; r; s; H].
 119   elim H ? ?; [split; assumption | exact r | exact s].
 120   qed.
 121
 122 theorem th10:
 123   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
 124   intros [P; Q; R; S; r; s; H].
 125   elim H ?; [split; assumption | exact r | exact s].
 126   qed.
 127
 128 theorem th11:
 129   \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
 130   intros [P; Q; R; S; r; s; H].
 131   elim H; [split; assumption | exact r | exact s].
 132   qed.
 133
 134
 135
 136
 137
 138
 139
 140
 141
 142