Commit 82720a0e authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Remove notations like =? in AsciiOrder and StringOrder

 These notations already exist in Coq 8.9, causing a nasty warning
parent f9858496
......@@ -28,12 +28,8 @@ Definition ascii_eqb c c' := (N_of_ascii c =? N_of_ascii c')%N.
Definition ascii_ltb c c' := (N_of_ascii c <? N_of_ascii c')%N.
Definition ascii_leb c c' := (N_of_ascii c <=? N_of_ascii c')%N.
Infix "<" := ascii_lt : char_scope.
Infix "<=" := ascii_le : char_scope.
Infix "?=" := ascii_compare (at level 70) : char_scope.
Infix "=?" := ascii_eqb : char_scope.
Infix "<?" := ascii_ltb : char_scope.
Infix "<=?" := ascii_leb : char_scope.
Local Infix "<" := ascii_lt.
Local Infix "<=" := ascii_le.
Lemma ascii_lt_strorder : StrictOrder ascii_lt.
Proof.
......@@ -49,25 +45,25 @@ Proof.
Qed.
Lemma ascii_compare_spec (c c' : ascii) :
CompareSpec (c=c') (c<c') (c'<c) (c ?= c').
CompareSpec (c=c') (c<c') (c'<c) (ascii_compare c c').
Proof.
unfold ascii_compare, ascii_lt.
case N.compare_spec; simpl; auto using ascii_N_inj.
Qed.
Lemma ascii_eqb_spec (c c' : ascii) : reflect (c = c') (c =? c').
Lemma ascii_eqb_spec c c' : reflect (c = c') (ascii_eqb c c').
Proof.
unfold ascii_eqb.
case N.eqb_spec; intros; simpl; constructor;
now rewrite <- ascii_N_iff.
Qed.
Lemma ascii_ltb_spec (c c' : ascii) : BoolSpec (c < c') (c' <= c) (c <? c').
Lemma ascii_ltb_spec c c' : BoolSpec (c < c') (c' <= c) (ascii_ltb c c').
Proof.
unfold ascii_ltb. case N.ltb_spec; simpl; auto.
Qed.
Lemma ascii_leb_spec (c c' : ascii) : BoolSpec (c <= c') (c' < c) (c <=? c').
Lemma ascii_leb_spec c c' : BoolSpec (c <= c') (c' < c) (ascii_leb c c').
Proof.
unfold ascii_leb. case N.leb_spec; simpl; auto.
Qed.
......
......@@ -7,6 +7,7 @@
Require Import Defs NameProofs Mix Meta Theories PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope string_scope.
Local Open Scope eqb_scope.
(** The Peano axioms *)
......@@ -87,7 +88,6 @@ Qed.
End PeanoAx.
Local Open Scope string.
Local Open Scope formula_scope.
Definition PeanoTheory :=
......@@ -389,16 +389,14 @@ Lemma PeanoFuns_ok s :
funsymbs PeanoSign s = get_arity (PeanoFuns s).
Proof.
unfold PeanoSign, peano_sign, PeanoFuns. simpl.
unfold eqb, eqb_inst_string.
repeat (case string_eqb; auto).
repeat (case eqbspec; auto); congruence.
Qed.
Lemma PeanoPreds_ok s :
predsymbs PeanoSign s = get_arity (PeanoPreds s).
Proof.
unfold PeanoSign, peano_sign, PeanoPreds. simpl.
unfold eqb, eqb_inst_string.
case string_eqb; auto.
repeat (case eqbspec; auto); congruence.
Qed.
Definition PeanoPreModel : PreModel nat PeanoTheory :=
......
......@@ -8,11 +8,14 @@ Require Import Bool Orders Ascii AsciiOrder String.
Local Open Scope string_scope.
Inductive string_lt : string -> string -> Prop :=
| LtEmpty a s : "" < String a s
| LtHead a a' s s' : (a < a')%char -> String a s < String a' s'
| LtTail a s s' : s < s' -> String a s < String a s'
where "u < v" := (string_lt u v) : string_scope.
| LtEmpty a s : string_lt "" (String a s)
| LtHead a a' s s' : ascii_lt a a' -> string_lt (String a s) (String a' s')
| LtTail a s s' : string_lt s s' -> string_lt (String a s) (String a s').
Hint Constructors string_lt.
Local Infix "<" := string_lt.
Definition string_le s s' := s<s' \/ s=s'.
Local Infix "<=" := string_le.
Lemma string_lt_strorder : StrictOrder string_lt.
Proof.
......@@ -23,9 +26,6 @@ Proof.
constructor. eapply ascii_lt_strorder; eauto.
Qed.
Definition string_le s s' := s<s' \/ s=s'.
Infix "<=" := string_le : string_scope.
Lemma string_le_lteq s s' : s<=s' <-> s<s' \/ s=s'.
Proof.
reflexivity.
......@@ -37,17 +37,15 @@ Fixpoint string_compare s s' :=
| "", _ => Lt
| _, "" => Gt
| String a s, String a' s' =>
match (a ?= a')%char with
match ascii_compare a a' with
| Eq => string_compare s s'
| Lt => Lt
| Gt => Gt
end
end.
Infix "?=" := string_compare (at level 70) : string_scope.
Lemma string_compare_spec s s' :
CompareSpec (s=s') (s<s') (s'<s) (s?=s').
CompareSpec (s=s') (s<s') (s'<s) (string_compare s s').
Proof.
revert s'.
induction s as [|a s IH]; destruct s' as [|a' s']; simpl; auto.
......@@ -56,28 +54,24 @@ Proof.
Qed.
Definition string_eqb s s' :=
match s ?= s' with
match string_compare s s' with
| Eq => true
| _ => false
end.
Definition string_ltb s s' :=
match s ?= s' with
match string_compare s s' with
| Lt => true
| _ => false
end.
Definition string_leb s s' :=
match s ?= s' with
match string_compare s s' with
| Gt => false
| _ => true
end.
Infix "=?" := string_eqb : string_scope.
Infix "<?" := string_ltb : string_scope.
Infix "<=?" := string_leb : string_scope.
Lemma string_eqb_spec (s s' : string) : reflect (s = s') (s =? s').
Lemma string_eqb_spec s s' : reflect (s = s') (string_eqb s s').
Proof.
unfold string_eqb.
assert (H := string_compare_spec s s').
......@@ -86,14 +80,14 @@ Proof.
intros <-. assert (~(s < s)) by apply string_lt_strorder. auto.
Qed.
Lemma string_ltb_spec (s s' : string) : BoolSpec (s < s') (s' <= s) (s <? s').
Lemma string_ltb_spec s s' : BoolSpec (s < s') (s' <= s) (string_ltb s s').
Proof.
unfold string_ltb, string_le.
assert (H := string_compare_spec s s').
destruct string_compare; constructor; inversion H; auto.
Qed.
Lemma string_leb_spec (s s' : string) : BoolSpec (s <= s') (s' < s) (s <=? s').
Lemma string_leb_spec s s' : BoolSpec (s <= s') (s' < s) (string_leb s s').
Proof.
unfold string_leb, string_le.
assert (H := string_compare_spec s s').
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment