Changeset 993 for src/ASM/Util.ma

Timestamp:

Jun 17, 2011, 6:28:49 PM (10 years ago)

Author:

sacerdot

Message:

More Russell everywhere; getting closer to the goal.

File:

• src/ASM/Util.ma (modified) (1 diff)

src/ASM/Util.ma

@@ -211 +211 @@
 for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
 
+axiom pair_elim':
+  ∀A,B,C: Type[0].
+  ∀T: A → B → C.
+  ∀p.
+  ∀P: A×B → C → Prop.
+    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
+      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
+
+axiom pair_elim'':
+  ∀A,B,C,C': Type[0].
+  ∀T: A → B → C.
+  ∀T': A → B → C'.
+  ∀p.
+  ∀P: A×B → C → C' → Prop.
+    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
+      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
+
+lemma pair_destruct_1:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
+ #A #B #a #b *; /2/
+qed.
+
+lemma pair_destruct_2:
+ ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
+ #A #B #a #b *; /2/
+qed.
+
+
 notation "⊥" with precedence 90
   for @{ match ? in False with [ ] }.