Equations on corelib

.vscode/settings.json

@@ -0,0 +1,13 @@
+{
+  "coqtop.binPath": "_opam/bin",
+  "coqtop.args": [
+
+    "-I", "_build/install/default/lib",
+    "-Q", "_build/default/theories", "Equations",
+    "-Q", "_build/default/examples", "Equations.Examples",
+    "-Q", "_build/default/test-suite", "Equations.TestSuite"
+  ],
+  "cSpell.enabledFileTypes": {
+    "coq": false
+  }
+}

Makefile

@@ -11,7 +11,7 @@ install:
 .PHONY: install
 
 test-suite:
-	dune build -p rocq-equations-tests
+	dune build -p rocq-equations,rocq-equations-examples,rocq-equations-tests
 
 .PHONY: test-suite
 

dune-project

@@ -21,18 +21,21 @@
   "logpath:Equations"))
  (depends
    (ocaml (>= 4.10.0))
-   (rocq-prover (>= "9.0~"))
+   (rocq-core (>= "9.0~"))
+   (coq-core (>= "9.0~")) ; For coqc shims for dune 
    (ppx_optcomp :build)
    (ocaml-lsp-server :with-dev-setup)))
 
 (package
  (name rocq-equations-examples)
  (synopsis "Examples")
  (description "Examples of use of Equations")
- (depends rocq-equations))
+ (depends rocq-equations
+  (rocq-stdlib (>= "9.0~"))))
 
 (package
  (name rocq-equations-tests)
  (synopsis "Technical package to run tests")
  (description "Do not install")
- (depends rocq-equations))
+ (depends rocq-equations
+  (rocq-stdlib (>= "9.0~"))))

examples/Basics.v

@@ -24,7 +24,7 @@
 
 #[warnings="-deprecated-library-file-since-8.20"]
 From Stdlib Require Import Program Bvector List Relations.
-From Equations Require Import Equations Signature.
+From Equations.Prop Require Import Equations.
 From Stdlib Require Import Utf8.
 
 Set Keyed Unification.
@@ -103,6 +103,7 @@ Module KAxiom.
       on closed or open terms. *)
 End KAxiom.
 
+
 Module KDec.
   (** However, types enjoying a provable instance of the [K] principle are fine using the [With UIP]
       option. Note that the following definition does *not* reduce according to its single clause

examples/Equations_Tutorial_VeriMag.v

@@ -413,6 +413,8 @@ Derive Signature for vec.
 Arguments nil {A}.
 Arguments cons {A n}.
 
+Declare Scope vector_scope.
+
 Notation "x :: v" := (cons x v) : vector_scope.
 Notation "[ ]" := nil : vector_scope.
 Notation "[ x ]" := (cons x nil) : vector_scope.

examples/Fin.v

@@ -9,6 +9,7 @@
 (** An example development of the [fin] datatype using [equations]. *)
 
 From Stdlib.Program Require Import Basics Combinators.
+From Stdlib Require Import Arith.
 From Equations.Prop Require Import Equations.
 Open Scope equations_scope.
 (** [fin n] is the type of naturals smaller than [n]. *)

examples/STLC.v

@@ -19,6 +19,8 @@ From Equations.Prop Require Import Equations.
 From Stdlib Require Import Lia List Utf8.
 Import ListNotations.
 
+Local Obligation Tactic := CoreTactics.equations_simpl.
+
 Set Keyed Unification.
 
 Derive Signature for le CompareSpec.
@@ -600,6 +602,9 @@ Definition her_type (t : type * term * term) :=
   let u' := fst (fst t) in
    { u : type | u = u' \/ type_subterm u u' }.
 
+
+Import Equations.Prop.Relations Equations.Prop.Subterm. (* For Equations's clos_trans and lexprod definitions *)
+
 #[local] Remove Hints t_step : subterm_relation.
 #[local] Remove Hints Subterm.clos_trans_stepr : subterm_relation.
 

examples/ho_finite_branching.v

@@ -1,8 +1,8 @@
 (** * Higher-order recursion, an example with finite branching trees *)
 
 From Equations.Prop Require Import Equations.
-
-Require Import Examples.Fin.
+From Equations Require Import Examples.Fin.
+Local Obligation Tactic := CoreTactics.equations_simpl.
 
 Inductive ho : Set :=
 | base : nat -> ho

examples/polynomials.v

@@ -24,7 +24,9 @@ From Stdlib Require Import ZArith Lia.
 From Stdlib Require Import Psatz.
 From Stdlib Require Import Nat.
 #[warnings="-warn-library-file-stdlib-vector"]
-Require Import Stdlib.Vectors.VectorDef.
+Require Import Stdlib.Vectors.Vector.
+
+Local Obligation Tactic := CoreTactics.equations_simpl.
 
 Set Keyed Unification.
 
@@ -262,7 +264,7 @@ Qed.
     We program [eval p v] where [v] is a valuation in [Z] for all the
     variables in [p : poly _ n]. *)
 
-Equations eval {n} {b} (p : poly b n) (v : Vector.t Z n) : Z :=
+Equations eval {n} {b} (p : poly b n) (v : VectorDef.t Z n) : Z :=
   eval poly_z         nil           := 0%Z;
   eval (poly_c z _)   nil           := z;
   eval (poly_l p)     (cons _ xs)   := eval p xs;

examples/wfrec.v

@@ -9,7 +9,7 @@
 
 From Equations.Prop Require Import Equations.
 From Stdlib Require Import List Syntax Arith Lia.
-From Stdlib Require Import List.
+Local Obligation Tactic := CoreTactics.equations_simpl.
 Import ListNotations.
 (* end hide *)
 (** * Well-founded recursion
@@ -77,7 +77,7 @@ Proof.
   auto.
 Qed.
 
-Equations ack (m n : nat) : nat by wf (m, n) (Equations.Prop.Subterm.lexprod _ _ lt lt) :=
+Equations ack (m n : nat) : nat by wf (m, n) (lexprod _ _ lt lt) :=
   ack 0 0         := 1;
   ack 0 (S n)     := S (S n);
   ack (S m) 0     := ack m 1;

test-suite/Basics.v

@@ -6,7 +6,8 @@
 (* GNU Lesser General Public License Version 2.1                      *)
 (**********************************************************************)
 
-From Stdlib Require Import Program List Relations.
+#[warnings="-warn-library-file-stdlib-vector"]
+From Stdlib Require Import Program Vector List Relations.
 From Equations.Prop Require Import Equations.
 
 From Stdlib Require Import Utf8.

test-suite/BasicsDec.v

@@ -46,7 +46,7 @@ Print Assumptions well_founded_t_subterm.
 Lemma well_founded_vector_direct_subterm' :
   forall A : Type, EqDec A -> WellFounded (t_subterm A).
 Proof. intros.
-  apply Transitive_Closure.wf_clos_trans.
+  apply Relations.wf_clos_trans.
   intro. simp_sigmas.
   induction a0; constructor; intros;
   simp_sigmas. simpl in *.

test-suite/fin.v

@@ -1,4 +1,4 @@
-From Stdlib Require Import Program.
+From Stdlib Require Import Program Arith.
 From Equations.Prop Require Import EqDecInstances Equations.
 Import Sigma_Notations.
 Local Open Scope equations_scope.

test-suite/nestedrec.v

@@ -1,5 +1,5 @@
 From Equations.Prop Require Import Equations.
-
+From Stdlib Require Import List.
 
 Inductive term : Set :=
 | Var (n : nat)

test-suite/rec.v

@@ -12,6 +12,8 @@ From Stdlib Require Import List Relations.
 From Stdlib Require Import Arith Wf_nat.
 From Stdlib Require Import Lia.
 
+Local Obligation Tactic := CoreTactics.equations_simpl.
+
 Module RecRel.
   Unset Equations With Funext.
 

test-suite/terms.v

@@ -1,4 +1,5 @@
 From Equations.Prop Require Import Equations.
+From Stdlib Require Import List.
 
 Inductive term :=
 | Var : nat -> term

theories/HoTT/Classes.v

@@ -8,7 +8,7 @@
 
 From Equations Require Import Init CoreTactics.
 Set Warnings "-notation-overridden".
-From Stdlib Require Import HoTT.Basics.Trunc HoTT.HSet.
+From Corelib Require Import HoTT.Basics.Trunc HoTT.HSet.
 From Equations Require Import HoTT.Logic Equations.HoTT.Relation
         Equations.HoTT.Relation_Properties Equations.HoTT.WellFounded.
 

theories/HoTT/DepElim.v

@@ -10,7 +10,7 @@
 
 Set Warnings "-notation-overridden".
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 Require Export Equations.Init.
 From Equations Require Import Signature CoreTactics.
 From Equations Require Import HoTT.Logic.

theories/HoTT/EqDec.v

@@ -232,7 +232,7 @@ Definition apd_eq {A} {x y : A} (p : x = y) {z} (q : z = x) :
   transport (@paths A z) p q = q @ p.
 Proof. now destruct p, q. Defined.
 
-From Stdlib Require Import HoTT.Basics.Trunc.
+From Corelib Require Import HoTT.Basics.Trunc.
 
 Lemma hprop_hset {A} (h : IsHProp A) : IsHSet A.
 Proof.

theories/HoTT/FunctionalInduction.v

@@ -9,7 +9,7 @@
 Set Warnings "-notation-overridden".
 From Equations Require Import CoreTactics.
 From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.DepElim.
-From Stdlib Require Import HoTT.Spaces.Nat.
+From Corelib Require Import HoTT.Spaces.Nat.
 
 Local Open Scope nat_scope.
 Local Open Scope equations_scope.

theories/HoTT/Logic.v

@@ -23,7 +23,7 @@ Register ap as core.identity.congr.
 
 Definition path_inspect {A : Type} (x : A) : { y | paths x y } := (x ; idpath).
 
-From Stdlib Require Import HoTT.Types.Bool.
+From Corelib Require Import HoTT.Types.Bool.
 (* For compatibility with Coq's [induction] *)
 Definition Bool_rect := Bool_ind.
 

theories/HoTT/NoConfusion.v

@@ -16,7 +16,7 @@ From Equations Require Import Init Signature.
 From Equations Require Import CoreTactics.
 From Equations Require Import HoTT.Logic Equations.HoTT.Classes Equations.HoTT.EqDec Equations.HoTT.Constants.
 From Equations Require Import HoTT.DepElim Equations.HoTT.Tactics.
-From Stdlib Require Import HoTT.Spaces.List.Core.
+From Corelib Require Import HoTT.Spaces.List.Core.
 
 
 (** Parameterized inductive types just need NoConfusion. *)

theories/HoTT/WellFounded.v

@@ -2,7 +2,7 @@ Set Warnings "-notation-overridden".
 From Equations Require Import Init CoreTactics.
 From Equations Require Import HoTT.Logic
         Equations.HoTT.Relation Equations.HoTT.Relation_Properties.
-From Stdlib Require Import HoTT.Basics.Tactics.
+From Corelib Require Import HoTT.Basics.Tactics.
 
 Set Universe Polymorphism.
 Import Sigma_Notations.

theories/Init.v

@@ -7,7 +7,6 @@
 (**********************************************************************)
 
 From Corelib Require Import Extraction.
-From Stdlib Require Import Unicode.Utf8_core.
 
 Declare ML Module "rocq-runtime.plugins.ltac".
 Declare ML Module "rocq-equations.plugin".

theories/Prop/Classes.v

@@ -7,7 +7,7 @@
 (**********************************************************************)
 
 From Equations Require Import Init CoreTactics.
-From Stdlib Require Import Extraction Relation_Definitions.
+From Corelib Require Import Extraction Relation_Definitions.
 From Equations.Prop Require Import Logic.
 
 (** A class for well foundedness proofs.

theories/Prop/Constants.v

@@ -1,6 +1,6 @@
 From Equations Require Import Init.
-From Equations.Prop Require Import Classes EqDec DepElim.
-From Stdlib Require Import Relations.
+From Equations.Prop Require Import Classes EqDec DepElim Relations.
+From Corelib Require Import Relation_Definitions.
 
 (** Naturals *)
 Register Init.Datatypes.O as equations.nat.zero.
@@ -52,7 +52,7 @@ Register Init.Datatypes.pair as equations.product.intro.
 Register Classes.WellFounded as equations.wellfounded.class.
 Register Init.Wf.well_founded as equations.wellfounded.type.
 Register Relations.Relation_Definitions.relation as equations.relation.type.
-Register Relation_Operators.clos_trans as equations.relation.transitive_closure.
+Register Equations.Prop.Relations.clos_trans as equations.relation.transitive_closure.
 
 (* Dependent elimination constants *)
 Register Equations.Prop.DepElim.solution_left as equations.depelim.solution_left.

theories/Prop/DepElim.v

@@ -8,7 +8,7 @@
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 Require Export Equations.Init.
 From Equations Require Import CoreTactics.
 From Equations Require Import Signature.

theories/Prop/Equations.v

@@ -13,7 +13,7 @@ From Equations.Prop Require Import Telescopes.
 
 #[export] Existing Instance wf_tele_measure.
 
-From Stdlib Require Import Program.Tactics.
+From Corelib Require Import Program.Tactics.
 
 (* program_solve_wf launches auto on well-founded and propositional (i.e. in Prop) goals *)
 

theories/Prop/FunctionalExtensionality.v

@@ -0,0 +1,26 @@
+(**********************************************************************)
+(* Equations                                                          *)
+(* Copyright (c) 2009-2020 Matthieu Sozeau <[email protected]> *)
+(**********************************************************************)
+(* This file is distributed under the terms of the                    *)
+(* GNU Lesser General Public License Version 2.1                      *)
+(**********************************************************************)
+
+From Corelib Require Import Relation_Definitions.
+Set Warnings "-notation-overridden".
+From Equations Require Import Init.
+From Equations.Prop Require Import Logic.
+
+(** The polymorphic equality type used by Equations when working with equality in Type. *)
+
+Section FunExt.
+  Context (A : Type) (B : A -> Type).
+
+  Definition functional_extensionality :=
+    forall (f g : forall x, B x), (forall x, f x = g x) -> f = g.
+
+End FunExt.
+
+Axiom funext : forall A B, functional_extensionality A B.
+
+Ltac extensionality x := eapply funext; intros x.

theories/Prop/Loader.v

@@ -8,7 +8,7 @@
 
 (** The set of libraries required to run Equations with all features. *)
 
-From Stdlib Require Import Extraction.
+From Corelib Require Import Extraction.
 
 (** This exports tactics *)
 Declare ML Module "rocq-equations.plugin".
@@ -20,7 +20,7 @@ Require Export Equations.Prop.Classes.
 From Equations.Prop Require Import DepElim Constants.
 Require Export Equations.Prop.EqDec.
 Require Export Equations.Prop.EqDecInstances.
-Require Export Equations.Prop.NoConfusion Equations.Prop.Subterm.
+Require Export Equations.Prop.NoConfusion Equations.Prop.Relations Equations.Prop.Subterm.
 Require Export Equations.Prop.Tactics.
 Require Export Equations.Prop.FunctionalInduction. (* funelim tactic *)
 

theories/Prop/Logic.v

@@ -1,7 +1,7 @@
 From Equations Require Import Init.
 From Equations.Prop Require Export SigmaNotations.
 
-From Stdlib Require Import Extraction Relation_Definitions.
+From Corelib Require Import Extraction Relation_Definitions.
 
 (** The regular dependent eliminator of equality *)
 Scheme eq_elim := Induction for eq Sort Type.

theories/Prop/NoConfusion.v

@@ -11,7 +11,7 @@
    on some equation. *)
 
 Set Warnings "-deprecated-since-8.20".   
-From Stdlib Require Import Program.Tactics Bvector List.
+From Corelib Require Import Program.Tactics ListDef.
 Set Warnings "deprecated-since-8.20".
 From Equations Require Import Init Signature.
 From Equations Require Import CoreTactics.

theories/Prop/NoCycle.v

@@ -55,7 +55,7 @@ Proof with trivial.
         + firstorder. }
 Qed.
 
-From Stdlib Require Import CRelationClasses.
+From Corelib Require Import CRelationClasses.
 
 #[export]
 Instance nlt_refl : Reflexive nlt.