Merge pull request #115 from coq-community/backport-master-8.15

Backport master fixes and improvements to 8.15

Author: palmskog

README.md

@@ -108,10 +108,11 @@ Namely, it contains instances for:
 
 - Peano naturals	(`Import Instances.Peano.`)
 - Z binary numbers	(`Import Instances.Z.`)
+- Lists    		(`Import Instances.Lists.`)
 - N binary numbers	(`Import Instances.N.`)
 - P binary numbers	(`Import Instances.P.`)
 - Rational numbers	(`Import Instances.Q.`)
-- Prop			(`Import Instances.Prop_ops.`)
+- Prop    		(`Import Instances.Prop_ops.`)
 - Booleans		(`Import Instances.Bool.`)
 - Relations		(`Import Instances.Relations.`)
 - all of the above	(`Import Instances.All.`)

meta.yml

@@ -109,10 +109,11 @@ documentation: |
   
   - Peano naturals	(`Import Instances.Peano.`)
   - Z binary numbers	(`Import Instances.Z.`)
+  - Lists    		(`Import Instances.Lists.`)
   - N binary numbers	(`Import Instances.N.`)
   - P binary numbers	(`Import Instances.P.`)
   - Rational numbers	(`Import Instances.Q.`)
-  - Prop			(`Import Instances.Prop_ops.`)
+  - Prop    		(`Import Instances.Prop_ops.`)
   - Booleans		(`Import Instances.Bool.`)
   - Relations		(`Import Instances.Relations.`)
   - all of the above	(`Import Instances.All.`)

src/aac_rewrite.ml

@@ -232,7 +232,8 @@ let aac_reflexivity : unit Proofview.tactic =
         mkApp (Coq.get_efresh (Theory.Stubs.lift_reflexivity),
 	       [| x; r; lift.e.Coq.Equivalence.eq; lift.lift; reflexive |])
       in
-      Unsafe.tclEVARS sigma 
+      Unsafe.tclEVARS sigma
+      <*> Coq.tclRETYPE lift_reflexivity
       <*> Tactics.apply lift_reflexivity
       <*> (let concl = Goal.concl goal in
            tclEVARMAP >>= fun sigma ->

theories/AAC.v

@@ -6,7 +6,7 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
-(** * Theory file for the aac_rewrite tactic
+(** * Theory for AAC Tactics
 
    We define several base classes to package associative and possibly
    commutative/idempotent operators, and define a data-type for reified (or
@@ -26,21 +26,19 @@
    where one occurrence of [+] operates on nat while the other one
    operates on positive. *)
 
-Require Import Arith NArith.
-Require Import List.
-Require Import FMapPositive FMapFacts.
-Require Import RelationClasses Equality.
-Require Export Morphisms.
-
-From AAC_tactics
-Require Import Utils Constants.
+From Coq Require Import Arith NArith List.
+From Coq Require Import FMapPositive FMapFacts RelationClasses Equality.
+From Coq Require Export Morphisms.
+From AAC_tactics Require Import Utils Constants.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
 
 Local Open Scope signature_scope.
 
-(** * Environments for the reification process: we use positive maps to index elements *)
+(** ** Environments for the reification process
+
+  We use positive maps to index elements. *)
 
 Section sigma.
   Definition sigma := PositiveMap.t.
@@ -57,8 +55,7 @@ Section sigma.
   Register sigma_empty as aac_tactics.sigma.empty.
 End sigma.
 
-
-(** * Classes for properties of operators *)
+(** ** Classes for properties of operators *)
 
 Class Associative (X:Type) (R:relation X) (dot: X -> X -> X) :=
   law_assoc : forall x y z, R (dot x (dot y z)) (dot (dot x y) z).
@@ -75,7 +72,6 @@ Register Commutative as aac_tactics.classes.Commutative.
 Register Idempotent as aac_tactics.classes.Idempotent.
 Register Unit as aac_tactics.classes.Unit.
 
-
 (** Class used to find the equivalence relation on which operations
    are A or AC, starting from the relation appearing in the goal *)
 
@@ -88,24 +84,21 @@ Register aac_lift_equivalence as aac_tactics.internal.aac_lift_equivalence.
 
 (** simple instances, when we have a subrelation, or an equivalence *)
 
-#[global]
-Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E}
-  {HR: @Transitive X R} {HER: subrelation E R}: AAC_lift  R E | 3.
+#[export] Instance aac_lift_subrelation {X} {R} {E} {HE: Equivalence E}
+ {HR: @Transitive X R} {HER: subrelation E R} : AAC_lift R E | 3.
 Proof.
   constructor; trivial.
   intros ? ? H ? ? H'. split; intro G.
    rewrite <- H, G. apply HER, H'.
    rewrite H, G. apply HER. symmetry. apply H'.
 Qed.
 
-#[global]
-Instance aac_lift_proper {X} {R : relation X} {E} {HE: Equivalence E}
-  {HR: Proper (E==>E==>iff) R}: AAC_lift  R E | 4 := {}.
-
+#[export] Instance aac_lift_proper {X} {R : relation X} {E}
+ {HE: Equivalence E} {HR: Proper (E==>E==>iff) R} : AAC_lift  R E | 4 := {}.
 
+(** ** Utilities for the evaluation function *)
 
 Module Internal.
-(** * Utilities for the evaluation function *)
 
 Section copy.
 
@@ -132,7 +125,7 @@ Section copy.
   Lemma copy_Psucc : forall n x, R (copy (Pos.succ n) x) (plus x (copy n x)).
   Proof. intros; unfold copy; rewrite Prect_succ. reflexivity. Qed.
 
-  Global Instance copy_compat n: Proper (R ==> R) (copy n).
+  #[export] Instance copy_compat n: Proper (R ==> R) (copy n).
   Proof.
     unfold copy.
     induction n using Pind; intros x y H.
@@ -142,9 +135,9 @@ Section copy.
 
 End copy.
 
-(** * Packaging structures *)
+(** ** Packaging structures *)
 
-(** ** free symbols  *)
+(** *** Free symbols  *)
 
 Module Sym.
   Section t.
@@ -189,7 +182,7 @@ Module Sym.
 
 End Sym.
 
-(** ** binary operations *)
+(** *** Binary operations *)
 
 Module Bin.
   Section t.
@@ -211,7 +204,7 @@ Module Bin.
 End Bin.
 
 
-(** * Reification, normalisation, and decision  *)
+(** ** Reification, normalisation, and decision  *)
 
 Section s.
   Context {X} {R: relation X} {E: @Equivalence X R}.
@@ -247,8 +240,9 @@ Section s.
   #[local]
   Hint Resolve e_bin e_unit: typeclass_instances.
 
-  (** ** Almost normalised syntax
-     a term in [T] is in normal form if:
+  (** *** Almost normalised syntax
+
+     A term in [T] is in normal form if:
      - sums do not contain sums
      - products do not contain products
      - there are no unary sums or products
@@ -303,7 +297,7 @@ Section s.
 
 
 
-  (** ** Evaluation from syntax to the abstract domain *)
+  (** *** Evaluation from syntax to the abstract domain *)
 
   Fixpoint eval u: X :=
     match u with
@@ -373,7 +367,7 @@ Section s.
     match Bin.idem (e_bin i) with Some _ => true | None => false end.
 
 
-  (** ** Normalisation *)
+  (** *** Normalisation *)
 
   #[universes(template)]
   Inductive discr {A} : Type :=
@@ -519,7 +513,7 @@ Section s.
       | vcons _ u l => vcons (norm u) (vnorm l)
     end.
 
-  (** ** Correctness *)
+  (** *** Correctness *)
 
   Lemma is_unit_of_Unit  : forall i j : idx,
    is_unit_of i j = true -> Unit R (Bin.value (e_bin i)) (eval (unit j)).
@@ -554,17 +548,16 @@ Section s.
   Proof.
     destruct ((e_bin i)); auto.
   Qed.
-  #[local]
-  Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative : core.
+  #[local] Hint Resolve Binvalue_Proper Binvalue_Associative Binvalue_Commutative : core.
 
   (** auxiliary lemmas about sums  *)
 
-  #[local]
-  Hint Resolve is_unit_of_Unit : core.
+  #[local] Hint Resolve is_unit_of_Unit : core.
   Section sum_correctness.
     Variable i : idx.
     Variable is_unit : idx -> bool.
-    Hypothesis is_unit_sum_Unit : forall j, is_unit j = true->  @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
+    Hypothesis is_unit_sum_Unit : forall j, is_unit j = true ->
+      @Unit X R (Bin.value (e_bin i)) (eval (unit j)).
 
     Inductive is_sum_spec_ind : T ->  @discr (mset T) -> Prop :=
     | is_sum_spec_op : forall j l, j = i -> is_sum_spec_ind (sum j l) (Is_op l)
@@ -974,8 +967,7 @@ Local Ltac internal_normalize :=
   compute [Internal.eval Utils.fold_map Internal.copy Prect]; simpl.
 
 
-(** * Lemmas for performing transitivity steps
-   given an instance of AAC_lift *)
+(** ** Lemmas for performing transitivity steps given an AAC_lift instance *)
 
 Section t.
   Context `{AAC_lift}.

theories/Caveats.v

@@ -6,21 +6,16 @@
 (*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
 (***************************************************************************)
 
-(** * Currently known caveats and limitations of the [aac_tactics] library.
-
-   Depending on your installation, either uncomment the following two
-   lines, or add them to your .coqrc files, replacing "."
-   with the path to the [aac_tactics] library
-*)
-
-Require NArith PeanoNat.
+(** * Currently known caveats and limitations of AAC Tactics *)
 
+From Coq Require NArith PeanoNat.
 From AAC_tactics Require Import AAC.
 From AAC_tactics Require Instances.
 
 (** ** Limitations *)
 
-(** *** 1. Dependent parameters
+(** *** Dependent parameters
+
    The type of the rewriting hypothesis must be of the form
 
    [forall (x_1: T_1) ... (x_n: T_n), R l r],
@@ -70,13 +65,14 @@ Section parameters.
 End parameters.
 
 
-(** *** 2. Exogeneous morphisms
+(** *** Exogeneous morphisms
 
    We do not handle `exogeneous' morphisms: morphisms that move from
    type [T] to some other type [T']. *)
 
 Section morphism.
   Import NArith PeanoNat.
+  Import Instances.N Instances.Peano.
   Open Scope nat_scope.
 
   (** Typically, although [N_of_nat] is a proper morphism from
@@ -115,7 +111,7 @@ Section morphism.
 End morphism.
 
 
-(** *** 3. Treatment of variance with inequations.
+(** *** Treatment of variance with inequations
 
    We do not take variance into account when we compute the set of
    solutions to a matching problem modulo AC. As a consequence,
@@ -145,11 +141,10 @@ Section ineq.
 
 End ineq. 
 
-
-
 (** ** Caveats  *)
 
-(** *** 1. Special treatment for units.
+(** *** Special treatment for units
+
    [S O] is considered as a unit for multiplication whenever a [Peano.mult]
    appears in the goal. The downside is that [S x] does not match [1],
    and [1] does not match [S(0+0)] whenever [Peano.mult] appears in
@@ -192,11 +187,12 @@ End Peano.
 
 
 
-(** *** 2. Existential variables.
-We implemented an algorithm for _matching_ modulo AC, not for
-_unifying_ modulo AC. As a consequence, existential variables
-appearing in a goal are considered as constants, they will not be
-instantiated. *)
+(** *** Existential variables
+
+  We implemented an algorithm for _matching_ modulo AC, not for
+  _unifying_ modulo AC. As a consequence, existential variables
+  appearing in a goal are considered as constants, they will not be
+  instantiated. *)
 
 Section evars.
   Import ZArith.
@@ -220,7 +216,7 @@ Section evars.
 End evars.
 
 
-(** *** 3. Distinction between [aac_rewrite] and [aacu_rewrite] *)
+(** *** Distinction between [aac_rewrite] and [aacu_rewrite] *)
 
 Section U.
   Context {X} {R} {E: @Equivalence X R}
@@ -255,7 +251,7 @@ Section U.
 
 End U.
 
-(** *** 4. Rewriting units *)
+(** *** Rewriting units *)
 Section V.
   Context {X} {R} {E: @Equivalence X R}
   {dot}  {dot_A: Associative R dot} {dot_Proper: Proper (R ==> R ==> R) dot}
@@ -283,8 +279,9 @@ Section V.
   Qed.
 End V.
 
-(** *** 5. Rewriting too much things.  *)
+(** *** Rewriting too many things  *)
 Section W.
+  Import Instances.Peano.
   Variables a b c: nat.
   Hypothesis H: 0 = c.
 
@@ -308,8 +305,9 @@ Section W.
 
 End W.
 
-(** *** 6. Rewriting nullifiable patterns.  *)
+(** *** Rewriting nullifiable patterns *)
 Section Z.
+  Import Instances.Peano.
 
 (** If the pattern of the rewritten hypothesis does not contain "hard"
 symbols (like constants, function symbols, AC or A symbols without
@@ -335,14 +333,12 @@ Goal a+b*c = c.
      *)
 Abort.
 
-(** **** If the pattern is a unit or can be instantiated to be equal
-   to a unit:
+(** *** If the pattern is a unit or can be instantiated to be equal to a unit
   
    The heuristic is to make the unit appear at each possible position
    in the term, e.g. transforming [a] into [1*a] and [a*1], but this
    process is not recursive (we will not transform [1*a]) into
    [(1+0*1)*a] *)
-
 Goal a+b+c = c.
 
   aac_instances H0 [mult].            
@@ -352,7 +348,10 @@ Goal a+b+c = c.
   (** 7 solutions, we miss solutions like [(a+b+c+0*(1+0*[]))]*)
 Abort.
 
-(** *** Another example of the former case is the following, where the hypothesis can be instantiated to be equal to [1] *)
+(** *** Another example of the former case
+ 
+  In the following, the hypothesis can be instantiated
+  to be equal to [1]. *)
 Hypothesis H : forall x y, (x+y)*x = x*x + y *x.
 Goal a*a+b*a + c = c.
   (** Here, only one solution if we use the aac_instance tactic  *)
@@ -371,4 +370,3 @@ still unclear how to handle properly this kind of situation : we plan
 to investigate on this in the future *)
 
 End Z.
-