almost string is orderType

src/Sorting.v

@@ -37,9 +37,8 @@ Module Sorting (s : SignatureParameter) (n : NamesParameter).
 
 Module MB := MergeBig s n.
 Include MB. 
-Locate mixin_of.
-Parameter mysort:orderType tt. (*pourquoi tt et pas autre chose?*)
-Parameter DefautltSort:mysort.
+(* Parameter mysort:orderType tt. (*pourquoi tt et pas autre chose?*)
+Parameter DefautltSort:mysort. *)
 
 
 Definition string_eqtype : eqType.
@@ -54,13 +53,51 @@ Definition string_eqtype : eqType.
 (* Lemma ltn_def (x y:string) : (ltb x y) = (~~String.eqb y x) && (leb x y).
 Admitted. *)
 
-(* Lemma sot : Order.Total.axioms_ tt string. Admitted.
+Definition string_lt : string -> string -> bool := 
+  fun s s' => match compare s s' with 
+  | Lt => true 
+  | _ => false 
+  end.
+
+Definition string_le : string -> string -> bool:= 
+  fun s s' => match compare s s' with 
+  | Gt => false 
+  | _ => true 
+  end.
+
+Lemma sot : Order.Total.axioms_ tt string.
+Print Order.Total.axioms_.
+eexists _ _ _ _ _.
+Unshelve.
+3:{eexists _. unfold Equality.axiom.
+  apply eqb_spec. }
+3:{simpl. eexists . 
+- instantiate (1:=string_le).
+instantiate (1:=string_lt).
+intros. unfold string_le, string_lt.
+destruct (x ?= y) eqn:H.
++ rewrite Bool.andb_true_r. 
+apply compare_eq_iff in H.
+subst x. 
+unfold eq_op. simpl.
+
+ Search ((_ != _)). 
+rewrite (contraFneq (b:=true)).
+auto.
+Search (comparison).
+Search (_ && true). simpl.
+simpl.
+intros. unfold Order.isPOrder.axioms_.   }
+2:{eexists _. intros P n x H. Print find_subdef. simpl. exact string. }
+
+
+ Admitted.
 Definition mysort:orderType tt. (*pourquoi tt et pas autre chose?*)
 Proof.
 exists string.
 apply sot.
 Defined.
-Definition DefautltSort:mysort:="default".  *)
+Definition DefautltSort:mysort:="default".   
 
 
 Definition EqDecS : forall x y : mysort, {x = y} + {x <> y}.
@@ -219,7 +256,7 @@ Fixpoint flatten (pattern:pat) : flat_pat :=
 (*flatten p est sorted*)
 
 
-(* Example ams : mysort := "a"%string.
+Example ams : mysort := "a"%string.
 Example bms : mysort := "b"%string.
 Example cms : mysort := "c"%string.
 Example dms : mysort := "d"%string.
@@ -229,9 +266,9 @@ Example mypattern : pat :=
     (or_pat (sname_pat ams) (sname_pat bms)) 
     (or_pat 
       (and_pat (sname_pat cms) (sname_pat dms))
-      (sname_pat ems)). *)
+      (sname_pat ems)).
 
-(* Compute (flatten mypattern). *)
+ Compute (flatten mypattern).