branch for universe

[helm.git] / matita / tests / metasenv_ordering.ma

diff --git a/matita/tests/metasenv_ordering.ma b/matita/tests/metasenv_ordering.ma
new file mode 100644 (file)
index 0000000..ff61c9d
--- /dev/null
+++ b/matita/tests/metasenv_ordering.ma
@@ -0,0 +1,139 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+
+include "coq.ma".
+
+alias num (instance 0) = "natural number".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+
+(* REWRITE *)
+
+theorem th1 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 2 = 2.
+   intros. split; split;
+   [ reflexivity
+   | rewrite > H;
+     [ reflexivity | exact nat | exact (0=0) | exact Type ]
+   ]
+qed.    
+    
+theorem th2 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 3 = 3.
+   intros. split. split.
+   focus 13.
+     rewrite > (H ?); [reflexivity | exact nat | exact (0=0) | exact Type].     
+   unfocus.
+   reflexivity.
+   reflexivity.
+qed.       
+    
+theorem th3 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 4 = 4.
+   intros. split. split.
+   focus 13.
+     rewrite > (H ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+   unfocus.     
+   reflexivity.
+   reflexivity.
+qed. 
+
+theorem th4 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 5 = 5.
+   intros. split. split.
+   focus 13.
+     rewrite > (H ? ? ?); [reflexivity | exact nat | exact (0=0) | exact Type].
+   unfocus.     
+   reflexivity.
+   reflexivity.
+qed. 
+
+(* APPLY *)
+
+theorem th5 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 6 = 6.
+   intros. split. split.
+   focus 13.
+     apply H; [exact nat | exact (0=0) | exact Type].
+   unfocus.     
+   reflexivity.
+   reflexivity.
+qed. 
+
+theorem th6 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 7 = 7.
+   intros. split. split.
+   focus 13.
+     apply (H ?); [exact nat | exact (0=0) | exact Type].
+   unfocus.     
+   reflexivity.
+   reflexivity.
+qed.
+      
+theorem th7 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 8 = 8.
+   intros. split. split.
+   focus 13.
+     apply (H ? ?); [exact nat | exact (0=0) | exact Type].
+   unfocus.     
+   reflexivity.
+   reflexivity.
+qed.     
+      
+theorem th8 : 
+   \forall P:Prop.
+   \forall H:(\forall G1: Set. \forall G2:Prop. \forall G3 : Type. 1 = 0). 
+   1 = 1 \land 1 = 0 \land 9 = 9.
+   intros. split. split.
+   focus 13.
+     apply (H ? ? ?); [exact nat | exact (0=0) | exact Type].
+   unfocus.     
+   reflexivity.
+   reflexivity.
+qed.
+
+(* ELIM *)
+
+theorem th9:
+  \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
+  intros (P Q R S r s H).
+  elim (H ? ?); [split; assumption | exact r | exact s].
+  qed.
+ 
+theorem th10:
+  \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
+  intros (P Q R S r s H).
+  elim (H ?); [split; assumption | exact r | exact s].
+  qed.
+  
+theorem th11:
+  \forall P,Q,R,S : Prop. R \to S \to \forall E:(R \to S \to P \land Q). P \land Q.
+  intros (P Q R S r s H).
+  elim H; [split; assumption | exact r | exact s].
+  qed.