moved on w string as a ordertype

src/Sorting.v

@@ -326,6 +326,23 @@ Lemma string_lt_trans : forall x y z:string, string_lt x y = true -> string_lt y
   unfold string_lt. rewrite Ht. auto.
   Qed.
 
+Lemma string_lt_trans_b : forall x y z:string, string_lt x y = false -> string_lt y z = false -> string_lt x z = false.
+  unfold string_lt.
+  intros x y z H H'.
+  destruct (x ?= y) eqn: E.
+  - apply compare_eq_iff in E. subst y.
+  destruct (x ?= z) eqn:E'.
+  + reflexivity.
+  + apply H'.
+  + reflexivity.
+  - discriminate H.
+  - destruct (y ?= z) eqn:E'.
+  + apply compare_eq_iff in E'. subst z.
+  rewrite E. reflexivity.
+  + discriminate H'.
+  + rewrite (gt_trans _ _ _ E E'). reflexivity.
+  Qed. 
+
 Definition meet_string (s1 s2 : string) : string :=
   if string_lt s1 s2 then s1 else s2.
 
@@ -420,14 +437,37 @@ Theorem POrder_is_lattice_string : forall G, Order.POrder_isLattice.axioms_ tt s
       * reflexivity.
     + rewrite E. reflexivity.
     + destruct (string_lt x z) eqn:E''.
-      * admit.
+      * set (contra := string_lt_trans_b _ _ _ E E').
+      rewrite contra in E''.
+      discriminate E''.
       * reflexivity. 
   - unfold associative, join_string. intros.
-  admit.
-  - unfold meet_string,join_string.  admit.
-  - unfold meet_string,join_string.  admit.
-  - simpl.  admit. 
-  Admitted.
+    destruct (string_lt x y) eqn:E; destruct (string_lt y z) eqn:E'.
+    + rewrite (string_lt_trans _ _ _ E E'). reflexivity. 
+    + rewrite E. reflexivity.
+    + reflexivity.
+    + rewrite E. destruct (string_lt x z) eqn:E''.
+    * set (contra := string_lt_trans_b _ _ _ E E').
+      rewrite contra in E''. discriminate E''.
+    * reflexivity.
+  - unfold meet_string,join_string. intros.
+    destruct (string_lt x y) eqn:E.
+    rewrite E. reflexivity.
+    rewrite string_lt_irreflexive. reflexivity.
+  - unfold meet_string,join_string. intros. 
+    destruct (string_lt x y) eqn:E.
+    rewrite string_lt_irreflexive. reflexivity.
+    rewrite E. reflexivity.
+  - simpl. intros. unfold Order.le,eq_op. simpl.
+    unfold string_le,meet_string. 
+    destruct (x ?= y) eqn:E.
+    + apply compare_eq_iff in E. subst y.
+    destruct (string_lt x x); rewrite eqb_refl; reflexivity.
+    + unfold string_lt. rewrite E. rewrite eqb_refl; reflexivity.
+    + unfold string_lt. rewrite E.
+    apply gt_implies_not_eq in E. 
+    rewrite eqb_sym. rewrite E. reflexivity.
+  Qed.
 
 Theorem commutative_meet_string: commutative meet_string.
   Proof.