Compile without Stdlib

Co-authored-by: Enrico Tassi <[email protected]>

Author: proux01

Makefile

@@ -1,62 +1,52 @@
 dune = dune $(1) $(DUNE_$(1)_FLAGS)
 
-elpi/dune: elpi/dune.in
-	@rm -f $@
-	@echo "; generated by make, do not edit" > $@
-	@if $$(coqc --version | grep -q "8.19\|8.20") ; then \
-	  sed -e 's/@@STDLIB_THEORY@@//' $< >> $@ ; \
-	else \
-	  sed -e 's/@@STDLIB_THEORY@@/(theories Stdlib)/' $< >> $@ ; \
-	fi
-	@chmod a-w $@
-
-all: elpi/dune theories-stdlib/dune
+all: theories-stdlib/dune
 	$(call dune,build)
 	$(call dune,build) builtin-doc
 .PHONY: all
 
-build-core: elpi/dune theories-stdlib/dune
+build-core: theories-stdlib/dune
 	$(call dune,build) theories
 	$(call dune,build) builtin-doc
 .PHONY: build-core
 
-build-apps: elpi/dune theories-stdlib/dune
+build-apps: theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name theories)
 .PHONY: build-apps
 
-build: elpi/dune theories-stdlib/dune
+build: theories-stdlib/dune
 	$(call dune,build) -p coq-elpi @install
 	$(call dune,build) builtin-doc
 .PHONY: build
 
 all-tests: test-core test-stdlib test-apps test-apps-stdlib
 .PHONY: all-tests
 
-test-core: elpi/dune theories-stdlib/dune
+test-core: theories-stdlib/dune
 	$(call dune,runtest) tests
 	$(call dune,build) tests
 .PHONY: test-core
 
-test-apps: elpi/dune theories-stdlib/dune
+test-apps: theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test-apps
 
-test-apps-stdlib: elpi/dune theories-stdlib/dune
+test-apps-stdlib: theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name tests-stdlib)
 .PHONY: test-apps-stdlib
 
-test-stdlib: elpi/dune theories-stdlib/dune
+test-stdlib: theories-stdlib/dune
 	$(call dune,build) tests-stdlib
 .PHONY: test-stdlib
 
 all-examples: examples examples-stdlib
 .PHONY: all-examples
 
-examples: elpi/dune theories-stdlib/dune
+examples: theories-stdlib/dune
 	$(call dune,build) examples
 .PHONY: examples
 
-examples-stdlib: elpi/dune theories-stdlib/dune
+examples-stdlib: theories-stdlib/dune
 	$(call dune,build) examples-stdlib
 .PHONY: examples-stdlib
 
@@ -88,7 +78,7 @@ clean:
 	$(call dune,clean)
 .PHONY: clean
 
-install: elpi/dune
+install:
 	$(call dune,install) coq-elpi
 .PHONY: install
 

apps/derive/elpi/eqbOK.elpi

@@ -15,7 +15,7 @@ add-reflect (type-param F) Correct Refl {{
      fun (a : lp:Type) (eqA: a -> a -> bool) (heqA : lp:(HeqA a eqA)) => lp:(R a eqA heqA)
   }} :-
   Type = sort (typ {coq.univ.new}),
-  HeqA = (a\eqA\ {{ forall x1 x2 : lp:a, reflect (@eq lp:a x1 x2) (lp:eqA x1 x2) }}),
+  HeqA = (a\eqA\ {{ forall x1 x2 : lp:a, lib:elpi.reflect (@eq lp:a x1 x2) (lp:eqA x1 x2) }}),
   @pi-trm `a` Type aa\a\
   @pi-decl `eqA` {{ lp:a -> lp:a -> bool }} eqA\
   @pi-decl `heqA` (HeqA a eqA) heqA\
@@ -56,7 +56,7 @@ main (const C) Prefix [CL] :- std.do! [
   std.assert-ok! (coq.typecheck Breflect _) "eqbOK generates illtyped term", 
   coq.ensure-fresh-global-id (Prefix ^ "eqb_OK") Namerf,
   X = (global (const C) : term),
-  coq.env.add-const Namerf Breflect {{ forall a b : lp:X, Bool.reflect (@eq lp:X a b) (lp:F a b) }} @opaque! Reflect,
+  coq.env.add-const Namerf Breflect {{ forall a b : lp:X, lib:elpi.reflect (@eq lp:X a b) (lp:F a b) }} @opaque! Reflect,
   CL = eqbok-for (const C) Reflect,
   coq.elpi.accumulate _ "derive.eqbOK.db" (clause _ _ CL),
 ].

apps/derive/elpi/tag.elpi

@@ -52,7 +52,7 @@ do-dummy-branch _ _ _ _ {{ Prop }}. % dummy
 % [do-branch InTerm Acc NewTem NewAcc] descends into a branch and puts Acc
 % in place of the dummy
 pred do-branch i:term, i:term, o:term, o:term.
-do-branch {{ Prop }} X X Y :- coq.reduction.lazy.norm {{ lp:X + 1 }} Y.
+do-branch {{ Prop }} X X Y :- coq.reduction.lazy.norm {{ Pos.add lp:X 1 }} Y.
 do-branch (fun N T F) X (fun N T R) Y :-
   @pi-decl N T x\ do-branch (F x) X (R x) Y.
 

apps/derive/theories/derive/EqdepFacts.v

@@ -0,0 +1,177 @@
+(* Borrowed from Stdlib.Logic.EqdepFacts *)
+
+Section Dependent_Equality.
+
+Variables (U : Type) (P : U -> Type).
+
+(** Dependent equality *)
+
+Inductive eq_dep (p : U) (x : P p) : forall q : U, P q -> Prop :=
+  eq_dep_intro : eq_dep p x p x.
+#[local] Hint Constructors eq_dep: core.
+
+Lemma eq_dep_sym (p q : U) (x : P p) (y : P q) :
+  eq_dep p x q y -> eq_dep q y p x.
+Proof. destruct 1; auto. Qed.
+
+Scheme eq_indd := Induction for eq Sort Prop.
+
+Inductive eq_dep1 (p : U) (x : P p) (q : U) (y : P q) : Prop :=
+  eq_dep1_intro : forall h : q = p, x = eq_rect _ _ y _ h -> eq_dep1 p x q y.
+
+Lemma eq_dep_dep1 (p q : U) (x : P p) (y : P q) :
+  eq_dep p x q y -> eq_dep1 p x q y.
+Proof.
+revert q x y; destruct 1.
+apply eq_dep1_intro with (eq_refl p).
+simpl; trivial.
+Qed.
+
+End Dependent_Equality.
+
+Arguments eq_dep  [U P] p x q _.
+Arguments eq_dep1 [U P] p x q y.
+
+Section Equivalences.
+
+Variable U : Type.
+
+Definition Eq_rect_eq_on (p : U) (Q : U -> Type) (x : Q p) :=
+  forall (h : p = p), x = eq_rect p Q x p h.
+Definition Eq_rect_eq := forall p Q x, Eq_rect_eq_on p Q x.
+
+Definition Eq_dep_eq_on (P : U -> Type) (p : U) (x : P p) :=
+  forall (y : P p), eq_dep p x p y -> x = y.
+Definition Eq_dep_eq := forall P p x, Eq_dep_eq_on P p x.
+
+Definition UIP_on_ (x y : U) (p1 : x = y) := forall (p2 : x = y), p1 = p2.
+Definition UIP_ := forall x y p1, UIP_on_ x y p1.
+
+Definition Streicher_K_on_ (x : U) (P : x = x -> Prop) :=
+  P (eq_refl x) -> forall p : x = x, P p.
+Definition Streicher_K_ := forall x P, Streicher_K_on_ x P.
+
+Lemma eq_rect_eq_on__eq_dep1_eq_on (p : U) (P : U -> Type) (y : P p) :
+  Eq_rect_eq_on p P y -> forall (x : P p), eq_dep1 p x p y -> x = y.
+Proof.
+intro eq_rect_eq.
+simple destruct 1; intro.
+rewrite <- eq_rect_eq; auto.
+Qed.
+Lemma eq_rect_eq__eq_dep1_eq :
+  Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.
+Proof.
+exact (fun eq_rect_eq P p y x =>
+  @eq_rect_eq_on__eq_dep1_eq_on p P x (eq_rect_eq p P x) y).
+Qed.
+
+Lemma eq_rect_eq_on__eq_dep_eq_on (p : U) (P : U -> Type) (x : P p) :
+  Eq_rect_eq_on p P x -> Eq_dep_eq_on P p x.
+Proof.
+intros eq_rect_eq; red; intros y H.
+symmetry; apply (eq_rect_eq_on__eq_dep1_eq_on _ _ _ eq_rect_eq).
+apply eq_dep_sym in H; apply eq_dep_dep1; trivial.
+Qed.
+Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.
+Proof.
+exact (fun eq_rect_eq P p x y =>
+  @eq_rect_eq_on__eq_dep_eq_on p P x (eq_rect_eq p P x) y).
+Qed.
+Lemma eq_dep_eq_on__UIP_on (x y : U) (p1 : x = y) :
+  Eq_dep_eq_on (fun y => x = y) x eq_refl -> UIP_on_ x y p1.
+Proof.
+intro eq_dep_eq; red.
+elim p1 using eq_indd.
+intros p2; apply eq_dep_eq.
+elim p2 using eq_indd.
+apply eq_dep_intro.
+Qed.
+Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.
+Proof.
+exact (fun eq_dep_eq x y p1 =>
+  @eq_dep_eq_on__UIP_on x y p1 (eq_dep_eq _ _ _)).
+Qed.
+
+Lemma Streicher_K_on__eq_rect_eq_on (p : U) (P : U -> Type) (x : P p) :
+  Streicher_K_on_ p (fun h => x = eq_rect _ P x _ h) -> Eq_rect_eq_on p P x.
+Proof.
+intro Streicher_K; red; intros.
+apply Streicher_K.
+reflexivity.
+Qed.
+Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.
+Proof.
+exact (fun Streicher_K p P x =>
+  @Streicher_K_on__eq_rect_eq_on p P x (Streicher_K p _)).
+Qed.
+End Equivalences.
+
+Arguments eq_dep  U P p x q _ : clear implicits.
+
+Set Implicit Arguments.
+
+Section EqdepDec.
+
+Variable A : Type.
+
+Let comp (x y y' : A) (eq1 : x = y) (eq2 : x = y') : y = y' :=
+  eq_ind _ (fun a => a = y') eq2 _ eq1.
+
+Remark trans_sym_eq (x y : A) (u : x = y) : comp u u = eq_refl y.
+Proof. now case u. Qed.
+
+Variables (x : A) (eq_dec : forall y : A, x = y \/ x <> y).
+
+Let nu (y : A) (u : x = y) : x = y :=
+  match eq_dec y with
+  | or_introl eqxy => eqxy
+  | or_intror neqxy => False_ind _ (neqxy u)
+  end.
+
+#[local] Lemma nu_constant (y:A) (u v:x = y) : nu u = nu v.
+Proof.
+unfold nu; destruct (eq_dec y) as [Heq|Hneq]; [reflexivity|].
+now case Hneq.
+Qed.
+
+Let nu_inv (y : A) (v : x = y) : x = y := comp (nu (eq_refl x)) v.
+
+Remark nu_left_inv_on (y : A) (u : x = y) : nu_inv (nu u) = u.
+Proof. case u; unfold nu_inv; apply trans_sym_eq. Qed.
+
+Theorem eq_proofs_unicity_on (y : A) (p1 p2 : x = y) : p1 = p2.
+Proof.
+elim (nu_left_inv_on p1).
+elim (nu_left_inv_on p2).
+now elim nu_constant with y p1 p2.
+Qed.
+
+Theorem K_dec_on (P : x = x -> Prop) (H : P (eq_refl x)) (p : x = x) : P p.
+Proof. now elim eq_proofs_unicity_on with x (eq_refl x) p. Qed.
+
+End EqdepDec.
+
+Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A) :
+  forall P : x = x -> Prop, P (eq_refl x) -> forall p : x = x, P p.
+Proof. exact (@K_dec_on A x (eq_dec x)). Qed.
+
+Section Eq_dec.
+
+Variables (A : Type) (eq_dec : forall x y : A, {x = y} + {x <> y}).
+
+Theorem K_dec_type (x : A) (P : x = x -> Prop) (H : P (eq_refl x)) (p : x = x) :
+  P p.
+Proof.
+elim p using K_dec; [|now trivial].
+now intros x0 y; case (eq_dec x0 y); [left|right].
+Qed.
+
+Theorem eq_rect_eq_dec : forall (p : A) (Q : A -> Type) (x : Q p) (h : p = p),
+  x = eq_rect p Q x p h.
+Proof. exact (Streicher_K__eq_rect_eq A K_dec_type). Qed.
+
+Theorem eq_dep_eq_dec : forall (P : A->Type) (p : A) (x y : P p),
+  eq_dep A P p x p y -> x = y.
+Proof. exact (eq_rect_eq__eq_dep_eq A eq_rect_eq_dec). Qed.
+
+End Eq_dec.

apps/derive/theories/derive/bcongr.v

@@ -8,7 +8,6 @@ From elpi.apps.derive.elpi Extra Dependency "bcongr.elpi" as bcongr.
 From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook.
 From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
-From Coq Require Export Bool.
 From elpi Require Export elpi.
 From elpi.apps Require Export derive.
 From elpi.apps Require Export derive.projK.

apps/derive/theories/derive/eq.v

@@ -6,11 +6,10 @@ From elpi.apps.derive.elpi Extra Dependency "eq.elpi" as eq.
 From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook.
 From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
-From Coq Require Import Bool.
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 
-From Coq Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat.
 
 Register Coq.Numbers.Cyclic.Int63.PrimInt63.eqb as elpi.derive.eq_unit63.
 Register Coq.Floats.PrimFloat.eqb as elpi.derive.eq_float64.

apps/derive/theories/derive/eqK.v

@@ -8,18 +8,19 @@ From elpi.apps.derive.elpi Extra Dependency "eqK.elpi" as eqK.
 From elpi.apps.derive.elpi Extra Dependency "derive_hook.elpi" as derive_hook.
 From elpi.apps.derive.elpi Extra Dependency "derive_synterp_hook.elpi" as derive_synterp_hook.
 
+From elpi.core Require Import Bool.  (* remove when requiring Rocq >= 9.0 *)
 From elpi Require Import elpi.
 From elpi.apps Require Import derive.
 From elpi.apps Require Import derive.bcongr derive.eq derive.isK.
 
 Definition eq_axiom T eqb :=
-  forall (x y : T), Bool.Bool.reflect (x = y) (eqb x y).
+  forall (x y : T), Datatypes.reflect (x = y) (eqb x y).
 
 Definition eq_axiom_at T eqb (x : T) :=
-  forall y, Bool.Bool.reflect (x = y) (eqb x y).
+  forall y, Datatypes.reflect (x = y) (eqb x y).
 
 Definition eq_axiom_on T eqb (x y : T) :=
-  Bool.Bool.reflect (x = y) (eqb x y).
+  Datatypes.reflect (x = y) (eqb x y).
 
 Register eq_axiom    as elpi.derive.eq_axiom.
 Register eq_axiom_at as elpi.derive.eq_axiom_at.

apps/derive/theories/derive/eqType_ast.v

@@ -1,5 +1,5 @@
 From elpi Require Import elpi.
-From Coq Require Import PrimInt63 PrimFloat.
+From elpi.core Require Import PrimInt63 PrimFloat.
 From elpi.apps Require Import derive.
 
 From elpi.apps.derive.elpi Extra Dependency "eqType.elpi" as eqType.

apps/derive/theories/derive/eqb.v

@@ -1,7 +1,7 @@
 From elpi Require Import elpi.
 From elpi.apps Require Import derive derive.param1.
-From Coq Require Import ssrbool ssreflect Uint63.
-From Coq Require Import PArith.
+From elpi.core Require Import ssrbool ssreflect PrimInt63.
+From elpi.core Require Import PosDef.
 
 From elpi.apps.derive.elpi Extra Dependency "fields.elpi" as fields.
 From elpi.apps.derive.elpi Extra Dependency "eqb.elpi" as eqb.