Changeset 2111 for src/common

Timestamp:

Jun 26, 2012, 5:30:41 PM (8 years ago)

Author:

sacerdot

Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

File:

• src/common/Identifiers.ma (modified) (1 diff)

src/common/Identifiers.ma

@@ -80 +80 @@
 @(eqb_elim x y P) [ /2 by / | * #H @F % #E destruct /2 by / ]
 qed.
+
+lemma eq_identifier_eq:
+  ∀tag: String.
+  ∀l.
+  ∀r.
+    eq_identifier tag l r = true → l = r.
+  #tag #l #r cases l cases r
+  #pos_l #pos_r
+  cases pos_l cases pos_r
+  [1:
+    #_ %
+  |2,3,4,7:
+    #p1_l normalize in ⊢ (% → ?);
+    #absurd destruct(absurd)
+  |5,9:
+    #p1_l #p1_r normalize in ⊢ (% → ?);
+    #relevant lapply (eqb_true_to_eq … relevant) #EQ >EQ %
+  |*:
+    #p_l #p_r normalize in ⊢ (% → ?);
+    #absurd destruct(absurd)
+  ]
+qed.
+
+axiom neq_identifier_neq:
+  ∀tag: String.
+  ∀l, r: identifier tag.
+    eq_identifier tag l r = false → (l = r → False).
 
 include "basics/deqsets.ma".