before outing the proofs

src/Sorting.v

@@ -272,15 +272,16 @@ Lemma string_lt_trans : forall x y z:string, string_lt x y = true -> string_lt y
   intros x y z H H'.
   apply string_lt_useful in H.
   apply string_lt_useful in H'.
-  unfold string_lt.
-  destruct (x ?= z) eqn:E.
-  - apply compare_eq_iff in E.
-  subst z. rewrite compare_antisym in H. apply (f_equal CompOpp) in H.
-  rewrite CompOpp_involutive in H. simpl in H. rewrite H in H'. discriminate H'. 
-  - auto.
-  - revert y z H H' E. induction x as [|cx sx IHx]; intros.
-  + simpl in E. destruct z; discriminate E.
-  + apply (IHx y z). Admitted. 
+  rewrite compare_antisym in H'. apply (f_equal CompOpp) in H'.
+  rewrite CompOpp_involutive in H'. simpl in H'.
+  rewrite compare_antisym in H. apply (f_equal CompOpp) in H.
+  rewrite CompOpp_involutive in H. simpl in H.
+  assert (Ht : (z ?= x) = Gt).
+  apply (gt_trans _ _ _ H' H).
+  rewrite compare_antisym in Ht. apply (f_equal CompOpp) in Ht.
+  rewrite CompOpp_involutive in Ht. simpl in Ht.
+  unfold string_lt. rewrite Ht. auto.
+  Qed.
 
 Definition meet_string (s1 s2 : string) : string :=
   if string_lt s1 s2 then s1 else s2.
@@ -368,18 +369,22 @@ simpl.
     * apply (string_lt__n_lt_implies_eq x y E E').
   - unfold associative,meet_string. intros.
     destruct (string_lt x y) eqn:E; destruct (string_lt y z) eqn:E'.
-    + rewrite E. Search (string_lt).  destruct (string_lt x z) eqn:E''.
+    + rewrite E. destruct (string_lt x z) eqn:E''.
       * reflexivity.
-    * 
-    + admit.
-    + reflexivity.
-    rewrite E. reflexivity. admit.
-  - unfold associative, join_string.
+      * set (H := string_lt_trans _ _ _ E E'). rewrite H in E''. discriminate E''.
+    + destruct (string_lt x z) eqn:E''.
+      * reflexivity.
+      * reflexivity.
+    + rewrite E. reflexivity.
+    + destruct (string_lt x z) eqn:E''.
+      * admit.
+      * reflexivity. 
+  - unfold associative, join_string. intros.
   admit.
-  - admit.
-  - admit.
-  - simpl.
-  auto. admit. }
+  - unfold meet_string,join_string.  admit.
+  - unfold meet_string,join_string.  admit.
+  - simpl.  admit. 
+  }
 
 3:{simpl.  eexists meet_string join_string. 
   - unfold commutative,meet_string. intros s1 s2.