Merge pull request #17 from coq-community/no-utf8

Remove UTF-8 use and local functional extensionality axiom

CHANGELOG.md

@@ -14,6 +14,12 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - Support for OCaml builds with Dune
 - Support for Coq builds with Dune
 
+### Fixed
+- Remove dependency on a local functional extensionality axiom
+
+### Removed
+- All uses of UTF-8
+
 ## [8.11.0] - 2020-01-31
 ### Fixed
 - Compatibility with Coq 8.11

README.md

@@ -137,7 +137,7 @@ The Coq definitions and proofs are located in the `coq` directory. The code loca
   * `Algorithms/KVSAlg1.v`: The definition and proof of algorithm 1 in the paper
   * `Algorithms/KVSAlg2.v`: The definition and proof of algorithm 2 in the paper
   * `Algorithms/KVSAlg3.v`: The definition and proof of algorithm 3 in the appendix
-  * `Algorithms/Extract.v`: The Coq file that extracts the algorithms
+  * `Algorithms/ExtractAlgorithm.v`: Extraction directives for extracting the algorithms to OCaml
   * `Examples/Clients.v`: Verified client program
   * `Examples/ListClient.v`: Verified client program
   * `Lib` (directory): General purpose Coq libraries

coq/Algorithms/KVSAlg1.v

@@ -1,15 +1,14 @@
-Require Import Coq.Unicode.Utf8.
-
-Require Import Coq.Init.Datatypes.
-Require Import Coq.Arith.Max.
-Require Import Coq.Lists.List.
-Require Import Program.Equality.
-Require Import Coq.Lists.ListSet.
-Require Import Coq.Program.Basics.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Arith.Peano_dec.
-Require Import Coq.Arith.Compare_dec.
-Require Import Coq.Arith.EqNat.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Arith.Max.
+From Coq Require Import Lists.List.
+From Coq Require Import Program.Equality.
+From Coq Require Import Lists.ListSet.
+From Coq Require Import Program.Basics.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Arith.Peano_dec.
+From Coq Require Import Arith.Compare_dec.
+From Coq Require Import Arith.EqNat.
+Import ListNotations.
 
 From Chapar Require Import Predefs.
 From Chapar Require Import KVStore.
@@ -237,9 +236,9 @@ Module KVSAlg1CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg1 SyntaxArg.
         rewrite N2; clear N2.
 
         assert (L: clock (alg_state (node_states s'' (label_node l))) n
-                       ≤ clock (alg_state (node_states s2 (label_node l'))) n
-                       ∧ (label_node l' = n ∧ label_is_put l'
-                          →  clock (alg_state (node_states s'' (label_node l))) n <
+                       <= clock (alg_state (node_states s2 (label_node l'))) n
+                       /\ (label_node l' = n /\ label_is_put l'
+                          ->  clock (alg_state (node_states s'' (label_node l))) n <
                             clock (alg_state (node_states s2 (label_node l'))) n)).
 
         clear M1.
@@ -2253,7 +2252,7 @@ Module KVSAlg1CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg1 SyntaxArg.
       assert (A3: 
                 (clock (label_post_state lp) (label_node lp) = clock (alg_state (node_states s1 n')) (label_node lp) + 1)
                 /\ (forall n, In n nids /\ (n <> label_node lp)->
-                              clock (label_post_state lp) n ≤ clock (alg_state (node_states s1 n')) n)).
+                              clock (label_post_state lp) n <= clock (alg_state (node_states s1 n')) n)).
         subv_in l' N2.
         inversion N2; simpl in *; try contradiction.
         subst s'0. subst a. subst s'5. subst s'4. subst s'3. subst s'2. subst v0. subst k0. subst n3. subst c0. subst n'0. subst s'1.

coq/Algorithms/KVSAlg2.v

@@ -1,14 +1,14 @@
-Require Import Coq.Unicode.Utf8.
-Require Import Coq.Init.Datatypes.
-Require Import Coq.Arith.Max. 
-Require Import Coq.Lists.List.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Arith.EqNat.
-Require Import Coq.Arith.Peano_dec.
-Require Import Coq.Arith.Compare_dec.
-Require Import Coq.Program.Basics.
-Require Import Coq.Arith.Lt.
-Require Import Coq.Arith.Le.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Arith.Max. 
+From Coq Require Import Lists.List.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Arith.EqNat.
+From Coq Require Import Arith.Peano_dec.
+From Coq Require Import Arith.Compare_dec.
+From Coq Require Import Program.Basics.
+From Coq Require Import Arith.Lt.
+From Coq Require Import Arith.Le.
+Import ListNotations.
 
 From Chapar Require Import Predefs.
 From Chapar Require Import extralib.
@@ -3756,7 +3756,7 @@ Module KVSAlg2CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg2 SyntaxArg.
       (step_star (init p) h s
        /\ label_is_put l
        /\ In l h)
-      -> label_clock l ≤ received (alg_state (node_states s n)) n.
+      -> label_clock l <= received (alg_state (node_states s n)) n.
 
     Proof.
       intros.
@@ -4498,7 +4498,7 @@ Module KVSAlg2CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg2 SyntaxArg.
                         rewrite B4 in *; clear B4. clear B11 B12 B13 B14.
                         rewrite B15 in A5; clear B15.
 
-                        assert (B5: label_clock l ≤ received (alg_state (node_states s2 n'')) (label_node l)).
+                        assert (B5: label_clock l <= received (alg_state (node_states s2 n'')) (label_node l)).
                           subst lc. inversion H13. simpl in *. subst n''. simpl in *. simpl_override. simpl. subst a. 
 
                           unfold guard_method in H17.
@@ -4553,7 +4553,7 @@ Module KVSAlg2CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg2 SyntaxArg.
                         rewrite B4 in *; clear B4. clear B11 B12 B13 B14.
                         rewrite B15 in A53; clear B15.
 
-                        assert (B5: label_clock l'' ≤ received (alg_state (node_states s2 n'')) (label_node l'')).
+                        assert (B5: label_clock l'' <= received (alg_state (node_states s2 n'')) (label_node l'')).
                           subst lc. inversion H13. simpl in *. subst n''. simpl in *. simpl_override. simpl. subst a. 
 
                           unfold guard_method in H18.

coq/Algorithms/KVSAlg3.v

@@ -1,12 +1,12 @@
-Require Import Coq.Unicode.Utf8.
-Require Import Coq.Init.Datatypes.
-Require Import Coq.Arith.Max. 
-Require Import Coq.Lists.List.
-Require Import Coq.Bool.Bool.
-Require Import Coq.Arith.EqNat.
-Require Import Coq.Arith.Peano_dec.
-Require Import Coq.Arith.Compare_dec.
-Require Import Coq.Program.Basics.
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import Arith.Max. 
+From Coq Require Import Lists.List.
+From Coq Require Import Bool.Bool.
+From Coq Require Import Arith.EqNat.
+From Coq Require Import Arith.Peano_dec.
+From Coq Require Import Arith.Compare_dec.
+From Coq Require Import Program.Basics.
+Import ListNotations.
 
 From Chapar Require Import Predefs.
 From Chapar Require Import extralib.
@@ -115,7 +115,7 @@ Module KVSAlg3CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg3 SyntaxArg.
       let as1 := alg_state ((node_states (init p)) n) in
       let as2 := alg_state ((node_states s) n) in
       step_star (init p) h s
-      -> forall k, entry_clock (store as2 k) ≤ rec as2 (entry_node (store as2 k)).
+      -> forall k, entry_clock (store as2 k) <= rec as2 (entry_node (store as2 k)).
 
     Proof.
       intros.
@@ -259,7 +259,7 @@ Module KVSAlg3CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg3 SyntaxArg.
     forall (p: ICExec.Syntax.PProg)(h: list Label)(s: State)(n: NId),
         let as2 := alg_state ((node_states s) n) in
         step_star (init p) h s
-        -> forall n', In n' nids -> dep as2 n' ≤ rec as2 n'.
+        -> forall n', In n' nids -> dep as2 n' <= rec as2 n'.
 
     Proof.
       intros p h s n as2 H n' Hi.
@@ -1058,9 +1058,9 @@ Module KVSAlg3CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg3 SyntaxArg.
         rewrite N2; clear N2.
 
         assert (L: dep (alg_state (node_states s'' (label_node l))) n
-                       ≤ dep (alg_state (node_states s2 (label_node l'))) n
-                       ∧ (label_node l' = n ∧ label_is_put l'
-                          →  dep (alg_state (node_states s'' (label_node l))) n <
+                       <= dep (alg_state (node_states s2 (label_node l'))) n
+                       /\ (label_node l' = n /\ label_is_put l'
+                          ->  dep (alg_state (node_states s'' (label_node l))) n <
                              dep (alg_state (node_states s2 (label_node l'))) n)).
 
         clear M1.
@@ -3065,7 +3065,7 @@ Module KVSAlg3CauseObl (SyntaxArg: SyntaxPar) <: CauseObl KVSAlg3 SyntaxArg.
       assert (A3: 
                 (dep (label_post_state lp) (label_node lp) = rec (alg_state (node_states s1 n')) (label_node lp) + 1)
                 /\ (forall n, In n nids ->
-                              dep (label_post_state lp) n ≤ rec (alg_state (node_states s1 n')) n)).
+                              dep (label_post_state lp) n <= rec (alg_state (node_states s1 n')) n)).
         subv_in l' N2.
         inversion N2; simpl in *; try contradiction.
         subst s'0. subst a. subst s'5. subst s'4. subst s'3. subst s'2. subst v0. subst k0. subst n3. subst c0. subst n'0. subst s'1.

coq/Examples/Clients.v

@@ -1,6 +1,6 @@
 From Chapar Require Import Predefs.
 From Chapar Require Import KVStore.
-Require Import Coq.Strings.String.
+From Coq Require Import String.
 From Chapar Require Import ReflectiveAbstractSemantics.
 From Chapar Require KVSAlg1 KVSAlg2 KVSAlg3.
 

coq/Framework/KVStore.v

@@ -1,6 +1,5 @@
 From Coq Require Import FunctionalExtensionality.
 From Coq Require Import Lia.
-From Coq Require Import Unicode.Utf8.
 From Coq Require Import Arith.EqNat.
 From Coq Require Import Arith.Peano_dec.
 From Coq Require Import Arith.Compare_dec.
@@ -11,6 +10,7 @@ From Coq Require Import Arith.Minus.
 
 From Coq Require Import Relations.Relation_Operators. (* For union and transitive closure. *)
 From Coq Require Import List. (* For In function. *)
+Import ListNotations.
 
 From Chapar Require Import Predefs.
 
@@ -2486,7 +2486,7 @@ Module InstConcExec (SyntaxArg: SyntaxPar)(Alg: AlgDef).
     forall s l s',
        step s l s'
       -> (latest_label s < label_num l 
-          /\ label_num l ≤ latest_label s').
+          /\ label_num l <= latest_label s').
 
     Proof.
       intros.

coq/Framework/ReflectiveAbstractSemantics.v

@@ -1,8 +1,11 @@
+From Coq Require Import FunctionalExtensionality.
+From Coq Require Import List.
+From Coq Require Import Lia.
+Import ListNotations.
+
 From Chapar Require Import Predefs.
 From Chapar Require Import KVStore.
 
-From Coq Require Import Lia.
-
 Module Type AbsExecCarrier (SyntaxArg : SyntaxPar).
   Module AbsExec := AbsExec SyntaxArg.
 End AbsExecCarrier.