From 152676cb1c8f12e206ca82b90c4b82791b45b92e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Tue, 25 Nov 2025 11:32:57 +0100
Subject: [PATCH] start mapping to rocq stdlib

---
 rocq/.gitignore  |  8 ++++++++
 rocq/Makefile    | 22 ++++++++++++++++++++++
 rocq/_CoqProject |  2 ++
 rocq/encoding.lp | 16 ++++++++++++++++
 rocq/mappings.lp | 36 ++++++++++++++++++++++++++++++++++++
 rocq/mappings.v  | 19 +++++++++++++++++++
 6 files changed, 103 insertions(+)
 create mode 100644 rocq/.gitignore
 create mode 100644 rocq/Makefile
 create mode 100644 rocq/_CoqProject
 create mode 100644 rocq/encoding.lp
 create mode 100644 rocq/mappings.lp
 create mode 100644 rocq/mappings.v

diff --git a/rocq/.gitignore b/rocq/.gitignore
new file mode 100644
index 0000000..e673e3d
--- /dev/null
+++ b/rocq/.gitignore
@@ -0,0 +1,8 @@
+.*.aux
+*.v
+!mappings.v
+*.vo*
+*.glob
+rocq.mk
+rocq.mk.conf
+.rocq.mk.d
diff --git a/rocq/Makefile b/rocq/Makefile
new file mode 100644
index 0000000..f613a80
--- /dev/null
+++ b/rocq/Makefile
@@ -0,0 +1,22 @@
+LPFILES := $(wildcard ../*.lp)
+VFILES := $(LPFILES:../%.lp=%.v)
+VOFILES := $(VFILES:%=%o)
+
+default: v
+
+v: $(VFILES)
+
+%.v: encoding.lp mappings.lp ../%.lp
+	lambdapi export -o stt_coq --encoding encoding.lp --use-notations --mapping mappings.lp --requiring mappings ../$*.lp > $@ #--renaming $(HOL2DK_DIR)/renaming.lp --requiring "$(REQUIRING)"
+
+clean-v:
+	rm -f $(VFILES)
+
+rocq.mk: _CoqProject
+	rocq makefile -f _CoqProject -o $@
+
+vo: rocq.mk
+	$(MAKE) -f rocq.mk
+
+clean-vo:
+	rm -f $(VOFILES)
diff --git a/rocq/_CoqProject b/rocq/_CoqProject
new file mode 100644
index 0000000..b870928
--- /dev/null
+++ b/rocq/_CoqProject
@@ -0,0 +1,2 @@
+-R . Stdlib
+.
diff --git a/rocq/encoding.lp b/rocq/encoding.lp
new file mode 100644
index 0000000..5ea7874
--- /dev/null
+++ b/rocq/encoding.lp
@@ -0,0 +1,16 @@
+// dk/lp symbols used for encoding simple type theory
+
+builtin "El" ≔ τ;
+builtin "Prf" ≔ π;
+
+// symbols with special notations in Coq
+builtin "Set" ≔ Set;
+builtin "prop" ≔ Prop;
+builtin "arr" ≔ ⤳;
+builtin "imp" ≔ ⇒;
+builtin "all" ≔ ∀;
+builtin "eq" ≔ =;
+builtin "or" ≔ ∨;
+builtin "and" ≔ ∧;
+builtin "ex" ≔ ∃;
+builtin "not" ≔ ¬;
diff --git a/rocq/mappings.lp b/rocq/mappings.lp
new file mode 100644
index 0000000..2230297
--- /dev/null
+++ b/rocq/mappings.lp
@@ -0,0 +1,36 @@
+// Prop.lp
+builtin "Prop" ≔ Prop;
+builtin "True" ≔ ⊤;
+builtin "I" ≔ ⊤ᵢ;
+builtin "False" ≔ ⊥;
+builtin "False_ind" ≔ ⊥ₑ;
+builtin "imp" ≔ ⇒;
+builtin "not" ≔ ¬;
+builtin "and" ≔ ∧;
+builtin "conj" ≔ ∧ᵢ;
+builtin "proj1" ≔ ∧ₑ₁;
+builtin "proj2" ≔ ∧ₑ₂;
+builtin "or" ≔ ∨;
+builtin "or_intro1" ≔ ∨ᵢ₁;
+builtin "or_intro2" ≔ ∨ᵢ₂;
+builtin "or_elim" ≔ ∨ₑ;
+builtin "ex_intro" ≔ ∃ᵢ;
+builtin "ex_elim" ≔ ∃ₑ;
+builtin "iff" ≔ ⇔;
+
+// Set.lp
+builtin "Type'" ≔ Set;
+builtin "nat" ≔ ι;
+builtin "el" ≔ el;
+
+// FOL.lp
+builtin "all" ≔ ∀;
+builtin "ex" ≔ ∃;
+
+// HOL.lp
+builtin "arr" ≔ ⤳;
+// Eq.lp
+builtin "eq" ≔ =;
+builtin "eq_refl" ≔ eq_refl;
+builtin "ind_eq" ≔ ind_eq;
+builtin "neq" ≔ ≠;
diff --git a/rocq/mappings.v b/rocq/mappings.v
new file mode 100644
index 0000000..2f541f2
--- /dev/null
+++ b/rocq/mappings.v
@@ -0,0 +1,19 @@
+(* Prop.lp *)
+Definition imp (p q : Prop) : Prop := p -> q.
+
+(* Set.lp *)
+Record Type' := { type :> Type; el : type }.
+
+(* Fol.lp *)
+Definition all {a : Set} (P: a -> Prop) : Prop := forall x:a, P x.
+
+(* Hol.lp *)
+Definition arr a (b : Type') := {| type := a -> b; el := fun _ => el b |}.
+Canonical arr.
+
+(* Eq.lp *)
+Lemma ind_eq : forall {a : Type'} {x y : a}, (x = y) -> forall p, (p y) -> p x.
+Proof.
+  intros a x y e p py. rewrite e. exact py.
+Qed.
+Definition neq {a : Type'} (x y : a) := ~ (x = y).