start mapping to rocq stdlib

Author: fblanqui

rocq/.gitignore

@@ -0,0 +1,8 @@
+.*.aux
+*.v
+!mappings.v
+*.vo*
+*.glob
+rocq.mk
+rocq.mk.conf
+.rocq.mk.d

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)

rocq/_CoqProject

@@ -0,0 +1,2 @@
+-R . Stdlib
+.

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" ≔ ¬;

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" ≔ ≠;

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).