string done as ordertype (with admits)

src/Sorting.v

@@ -122,6 +122,27 @@ Proof.
   reflexivity.
 Qed.
 
+Lemma gt_implies_not_eq : forall x x', compare x x' = Gt -> String.eqb x x' = false.
+Proof.
+  intros. revert x' H.
+  induction x; intros.
+  simpl in *.
+  induction x'.
+  discriminate H.
+  reflexivity.
+  induction x'.
+  auto.
+  simpl.
+  destruct (Ascii.eqb a a0) eqn:E.
+  rewrite Ascii.eqb_eq in E.
+  subst a0.
+  apply (IHx x').
+  simpl in H.
+  rewrite ascii_compare_eq in H.
+  apply H.
+  reflexivity.
+Qed.
+
 Lemma string_lt_not_eq : forall s s',
   string_lt s s' = true ->  negb (String.eqb s s') .
 Proof.
@@ -144,6 +165,28 @@ Proof.
     + auto.    
   Qed.
 
+Lemma string_gt_not_eq : forall s s',
+  (s ?= s') = Gt ->  String.eqb s' s = false .
+Proof.
+  intros s s' H.
+  destruct (compare s s') eqn:Hcomp ; simpl in *.
+  - discriminate H.
+  - discriminate H. 
+  - destruct s as [|c sq]; destruct s' as [|c' sq'].
+    + discriminate Hcomp.
+    + auto.
+    + auto. 
+    + simpl in *.
+      destruct (Ascii.eqb c' c) eqn:E.
+      * apply Ascii.eqb_eq in E.
+        subst c.
+        rewrite ascii_compare_eq in Hcomp.
+        unfold is_true,negb.
+        apply gt_implies_not_eq in Hcomp.
+        rewrite eqb_sym. auto.
+      * auto.
+  Qed.
+
 Definition string_le : string -> string -> bool:= 
   fun s s' => match compare s s' with 
   | Gt => false 
@@ -289,13 +332,10 @@ Definition meet_string (s1 s2 : string) : string :=
 Definition join_string (s1 s2 : string) : string :=
   if string_lt s1 s2 then s2 else s1.
 
-
-Lemma sot : Order.Total.axioms_ tt string.
-eexists _ _ _ _ _.
-Unshelve.
-3:{eexists _. unfold Equality.axiom.
-  apply eqb_spec. }
-3:{simpl. eexists string_le string_lt. 
+Theorem POrder_axioms_string : Order.isPOrder.axioms_ tt string
+  {| hasDecEq.eq_op := String.eqb; hasDecEq.eqP := eqb_spec |}. 
+  Proof.
+  eexists string_le string_lt. 
   - intros. 
   unfold string_le, string_lt. 
   destruct (x ?= y) eqn:H.
@@ -343,10 +383,13 @@ Unshelve.
     apply (gt_trans _ _ _ E) in E'.
     rewrite E' in E''. discriminate E''.
 
-    apply H'. }
+    apply H'.
+  Defined.
 
-simpl.
-3:{simpl.  eexists meet_string join_string. 
+Theorem POrder_is_lattice_string : forall G, Order.POrder_isLattice.axioms_ tt string G
+{| hasDecEq.eq_op := String.eqb; hasDecEq.eqP := eqb_spec |} POrder_axioms_string.
+  Proof.
+  eexists meet_string join_string. 
   - unfold commutative,meet_string. intros.
     destruct (string_lt x y) eqn:E.
     + apply string_lt_antisymmetric in E.
@@ -384,108 +427,125 @@ simpl.
   - 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.
-    (* induction s2 as [|c2 s2' IHs2]; *)
-    revert s2.
-    induction s1 as [|c1 s1' IHs1]; intros.
-    + destruct s2. 
-      * reflexivity.
-      * reflexivity.
-    + destruct s2 as [|c2 s2'].
-      * reflexivity.
-      * destruct (Ascii.eqb c1 c2) eqn:E.
-      ** apply Ascii.eqb_eq in E.
-        subst c2.
-        rewrite Ascii.eqb_refl.
-        rewrite IHs1. reflexivity.
-      ** rewrite Ascii.eqb_sym.
-        rewrite E. reflexivity.
-  - admit.
-    (* unfold commutative,join_string. intros.
-    assert (Hassert:forall x' y':string, string_lt x' y' = true -> ~~ string_lt y' x'). { admit. }
-    destruct (string_lt x y) eqn:E.
-    + apply Hassert in E.
-    unfold is_true in E.
-    apply Bool.negb_true_iff in E.
-    rewrite E. reflexivity.
-    + apply Bool.negb_true_iff in E.
-    assert (Hassert':forall x' y':string, ~~ string_lt x' y' = true -> string_lt y' x'). { admit. }
-    apply Hassert' in E.
-    rewrite E. reflexivity. *)
-  - unfold associative ,meet_string. intros s1 s2 s3.
-    revert s2 s3.
-    induction s1 as [|c1 s1' IHs1]; intros.
-    + destruct s2 as [|c2 s2']; destruct s3 as [|c3 s3']; auto. 
-      destruct (Ascii.eqb c2 c3) eqn:E; auto.
-    + destruct s2 as [|c2 s2']; destruct s3 as [|c3 s3']; auto.
-       specialize (IHs1 s2' ""). simpl in IHs1.
   Admitted.
-       (* apply IHs1.
-    auto. 
-    destruct s3. auto. simpl. 
-    destruct (string_lt x y) eqn:E; destruct (string_lt y z) eqn:E'.
-    rewrite E.
-    + admit.
-    + reflexivity.
-    rewrite E. reflexivity. admit.
-  - unfold associative, join_string.
-  admit.
-  - admit.
-  - admit.
-  - simpl.
-  auto. admit. } *)
 
-(* 3:{simpl.  eexists meet_string join_string. 
-  - unfold commutative,meet_string. intros.
-    destruct (string_le x y) eqn:E.
+Theorem commutative_meet_string: commutative meet_string.
+  Proof. 
+    unfold commutative,meet_string. intros.
+    destruct (string_lt x y) eqn:E.
     + apply string_lt_antisymmetric in E.
     rewrite E. reflexivity.
     + apply Bool.negb_true_iff in E.
-    unfold negb in E. destruct (string_lt x y) eqn:E'. discriminate E. 
-    assert (Hassert':forall x' y':string, string_lt x' y' = false -> string_lt y' x' = true). { admit. }
-    apply Hassert' in E'.
-    rewrite E'. reflexivity.
-  - unfold commutative,join_string. intros.
-    assert (Hassert:forall x' y':string, string_lt x' y' = true -> ~~ string_lt y' x'). { admit. }
+    unfold negb in E. destruct (string_lt x y) eqn:E'. 
+    * discriminate E.
+    * destruct (string_lt y x) eqn:E''.
+    ** reflexivity.
+    ** symmetry.
+    apply (string_lt__n_lt_implies_eq x y E' E''). 
+  Qed.
+
+Theorem commutative_join_string: commutative join_string.
+  Proof. 
+    unfold commutative,join_string. intros.
     destruct (string_lt x y) eqn:E.
-    + apply Hassert in E.
+    + apply string_lt_imp_n_string_lt_opp in E.
     unfold is_true in E.
     apply Bool.negb_true_iff in E.
     rewrite E. reflexivity.
-    + apply Bool.negb_true_iff in E.
-    assert (Hassert':forall x' y':string, ~~ string_lt x' y' = true -> string_lt y' x'). { admit. }
-    apply Hassert' in E.
-    rewrite E. reflexivity.
-  - unfold associative,meet_string. intros.
+    + destruct (string_lt y x) eqn:E'.
+    * reflexivity.
+    * apply (string_lt__n_lt_implies_eq x y E E').
+  Qed.
+
+Theorem associative_meet_string: associative meet_string.
+  Proof.
+    unfold associative,meet_string. intros.
     destruct (string_lt x y) eqn:E; destruct (string_lt y z) eqn:E'.
-    rewrite E.
-    + admit.
-    + reflexivity.
-    rewrite E. reflexivity. admit.
-  - unfold associative, join_string.
-  admit.
-  - admit.
-  - admit.
-  - simpl.
-  auto. admit. } *)
+    + rewrite E. destruct (string_lt x z) eqn:E''.
+      * reflexivity.
+      * 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. 
+  Admitted.
+
+Theorem associative_join_string: associative join_string.
+  Proof. 
+    unfold associative, join_string. intros.
+  Admitted.
+
+Theorem meet_join_thm1 : forall y x : string, meet_string x (join_string x y) = x.
+  Admitted.
+
+Theorem join_meet_thm2 : forall y x : string, join_string x (meet_string x y) = x.
+  Admitted.
+
+(* Theorem meet_eq : forall x y : string, (x <= y)%O = (meet_string x y == x). *) 
+
+Theorem string_has_choice : hasChoice.axioms_ string. Admitted.
+
+Theorem meet_join_left_distr : forall x y z : string, meet_string (join_string x y) z = join_string (meet_string x z) (meet_string y z).  
+  Admitted.
+
+Theorem total_string : @total string
+  (@Order.le tt
+  (@Order.POrder.Pack tt string
+  (@Order.POrder.Class tt string string_has_choice
+  (@hasDecEq.Axioms_ string String.eqb eqb_spec) POrder_axioms_string))).
+  Admitted.
+
+Lemma sot : Order.Total.axioms_ tt string.
+eexists _ _ _ _ _.
+Unshelve.
+3:{eexists _. unfold Equality.axiom.
+  apply eqb_spec. }
+3:{simpl. apply POrder_axioms_string. }
+simpl.
+3:{simpl. 
+  eexists meet_string join_string. 
+  - apply commutative_meet_string.
+  - apply commutative_join_string.
+  - apply associative_meet_string.
+  - apply associative_join_string.
+  - apply meet_join_thm1.
+  - apply join_meet_thm2.
+  - simpl. intros. unfold meet_string. 
+  unfold Order.le.
+  simpl.
+  unfold string_le.
+  unfold eq_op. simpl.
+  destruct (string_lt x y) eqn:E.
+  + rewrite eqb_refl.
+    apply string_lt_implies_string_le in E.
+    unfold string_le in E.
+    destruct (x ?= y) eqn:H.
+    * reflexivity.
+    * reflexivity.
+    * apply E.
+  + destruct (x ?= y) eqn:H.
+    * apply compare_eq_iff in H. subst y. rewrite eqb_refl. reflexivity.
+    * exfalso. unfold string_lt in E. destruct (x ?= y). ** discriminate H. ** discriminate E. ** discriminate H.
+    * symmetry. apply (string_gt_not_eq _ _ H). }
+simpl.
+3:{simpl. eexists . simpl. unfold left_distributive, Order.meet, Order.join. simpl.
+  apply meet_join_left_distr. }  
+2:{apply string_has_choice. }
+simpl. eexists.  apply total_string.
+Defined.
 
-(* simpl.
-admit.
-admit.
-admit. 
-Admitted. *)
 
 
-Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N.
+(* Lemma ltn_def x y : (x < y)%N = (y != x) && (x <= y)%N.
 Admitted.
 
 #[export]
 HB.instance Definition _ :=
   Order.isOrder.Build tt nat ltn_def (fun _ _ => erefl) (fun _ _ => erefl)
-                anti_leq leq_trans leq_total.
+                anti_leq leq_trans leq_total. *)
 
 
 Definition mysort:orderType tt. (*pourquoi tt et pas autre chose?*)
@@ -516,7 +576,7 @@ Definition relSort: rel mysort.
     destruct class.
     destruct eqtype_hasDecEq_mixin.
     exact eq_op.
-  Qed.
+  Defined.
 
 
 Inductive pat : Type :=