mapping to rocq stdlib

rocq/.gitignore

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

rocq/Makefile

@@ -0,0 +1,61 @@
+.PREFIX:
+
+.PHONY: default
+default:
+	$(MAKE) dk
+	$(MAKE) v
+	$(MAKE) vo
+
+LPFILES := $(wildcard ../*.lp)
+DKFILES := $(LPFILES:../%.lp=%.dk)
+
+.PHONY: dk
+dk: $(DKFILES)
+
+%.dk: ../%.lp
+	lambdapi export -o dk $< > $@
+
+.PHONY: clean-dk
+clean-dk: clean-dko clean-v
+	-rm -f $(DKFILES) dko.mk
+
+.PHONY: dko
+dko: $(DKFILES:%.dk=%.dko)
+
+%.dko: %.dk
+	dk check -e $<
+
+include dko.mk
+
+dko.mk: $(DKFILES)
+	dk dep $(DKFILES) > $@
+
+.PHONY: clean-dko
+clean-dko:
+	-rm -f *.dko
+
+VFILES := $(DKFILES:%.dk=%.v)
+
+.PHONY: v
+v: $(VFILES)
+
+%.v: encoding.lp mapping.lp renaming.lp %.dk
+	lambdapi export -o stt_coq --encoding encoding.lp --renaming renaming.lp --mapping mapping.lp --requiring mapping --use-notations $*.dk > $@
+
+.PHONY: clean-v
+clean-v: clean-vo
+	-rm -f $(VFILES) rocq.mk rocq.mk.conf *.glob
+
+rocq.mk: _CoqProject
+	rocq makefile -f _CoqProject -o $@
+
+.PHONY: vo
+vo: rocq.mk
+	$(MAKE) -f rocq.mk
+
+.PHONY: clean-vo
+clean-vo:
+	rm -f *.vo*
+
+.PHONY: clean
+clean: clean-dk

rocq/_CoqProject

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

rocq/encoding.lp

@@ -0,0 +1,15 @@
+// symbols used for encoding simple type theory
+
+builtin "El" ≔ {|τ|};
+builtin "Prf" ≔ {|π|};
+
+builtin "Set" ≔ Set;
+builtin "prop" ≔ Prop;
+builtin "arr" ≔ {|⤳|};
+builtin "imp" ≔ {|⇒|};
+builtin "all" ≔ {|∀|};
+builtin "eq" ≔ =;
+builtin "or" ≔ {|∨|};
+builtin "and" ≔ {|∧|};
+builtin "ex" ≔ {|∃|};
+builtin "not" ≔ {|¬|};

rocq/mapping.lp

@@ -0,0 +1,100 @@
+// Prop
+builtin "Prop" ≔ Prop.Prop;
+builtin "True" ≔ Prop.{|⊤|};
+builtin "I" ≔ Prop.{|⊤ᵢ|};
+builtin "False" ≔ Prop.{|⊥|};
+builtin "False_ind" ≔ Prop.{|⊥ₑ|};
+builtin "imp" ≔ Prop.{|⇒|};
+builtin "not" ≔ Prop.{|¬|};
+builtin "and" ≔ Prop.{|∧|};
+builtin "conj" ≔ Prop.{|∧ᵢ|};
+builtin "proj1" ≔ Prop.{|∧ₑ₁|};
+builtin "proj2" ≔ Prop.{|∧ₑ₂|};
+builtin "\/" ≔ Prop.{|∨|};
+builtin "or_intro1" ≔ Prop.{|∨ᵢ₁|};
+builtin "or_intro2" ≔ Prop.{|∨ᵢ₂|};
+builtin "or_elim" ≔ Prop.{|∨ₑ|};
+builtin "ex_intro" ≔ Prop.{|∃ᵢ|};
+builtin "ex_elim" ≔ Prop.{|∃ₑ|};
+builtin "iff" ≔ Prop.{|⇔|};
+
+// Set
+builtin "Type'" ≔ Set.Set;
+builtin "nat" ≔ Set.{|ι|};
+builtin "el" ≔ Set.el;
+
+// Prod
+builtin "prod" ≔ Prod.{|×|};
+builtin "pair" ≔ Prod.{|‚|};
+builtin "fst" ≔ Prod.{|₁|};
+builtin "snd" ≔ Prod.{|₂|};
+
+// FOL
+builtin "all" ≔ FOL.{|∀|};
+builtin "ex" ≔ FOL.{|∃|};
+
+// HOL
+builtin "arr" ≔ HOL.{|⤳|};
+
+// Eq
+builtin "eq" ≔ Eq.=;
+builtin "eq_refl" ≔ Eq.eq_refl;
+builtin "ind_eq" ≔ Eq.ind_eq;
+builtin "neq" ≔ Eq.{|≠|};
+
+// Bool
+builtin "bool'" ≔ Bool.{|𝔹|};
+builtin "bool'" ≔ Bool.bool;
+builtin "Is_true" ≔ Bool.istrue;
+builtin "negb" ≔ Bool.not;
+builtin "orb" ≔ Bool.or;
+builtin "andb" ≔ Bool.and;
+builtin "if'" ≔ Bool.if;
+
+// Classic
+builtin "classic" ≔ Classic.em; 
+
+// Comp
+builtin "comparison'" ≔ Comp.comp;
+builtin "comparison'" ≔ Comp.Comp;
+builtin "CompOpp" ≔ Comp.opp;
+builtin "isEq" ≔ Comp.isEq;
+builtin "isLt" ≔ Comp.isLt;
+builtin "isGT" ≔ Comp.isGt;
+builtin "case_Comp" ≔ Comp.case_Comp;
+
+// Epsilon
+builtin "eps" ≔ Epsilon.{|ε|};
+builtin "eps_spec" ≔ Epsilon.{|εᵢ|};
+
+// Nat
+builtin "nat" ≔ Nat.{|ℕ|};
+builtin "O" ≔ Nat._0;
+builtin "S" ≔ Nat.+1;
+builtin "Nat.add" ≔ Nat.+;
+builtin "Nat.sub" ≔ Nat.-;
+builtin "Nat.pred" ≔ Nat.{|∸1|};
+builtin "Nat.mul" ≔ Nat.*;
+builtin "Nat.leb" ≔ Nat.{|≤|};
+builtin "Nat.ltb" ≔ Nat.<;
+
+// List
+builtin "List" ≔ List.{|𝕃|};
+builtin "nil" ≔ List.{|□|};
+builtin "cons" ≔ List.{|⸬|};
+builtin "List.In" ≔ List.{|∈|};
+builtin "app" ≔ List.++;
+
+// Pos
+builtin "positive" ≔ Pos.{|ℙ|};
+builtin "xI" ≔ Pos.I;
+builtin "xO" ≔ Pos.O;
+builtin "xH" ≔ Pos.H;
+
+// Z
+builtin "Z" ≔ Z.{|ℤ|};
+builtin "Z0" ≔ Z.Z0;
+builtin "Zpos" ≔ Z.Zpos;
+builtin "Zneg" ≔ Z.Zneg;
+builtin "Z.opp" ≔ Z.{|—|};
+builtin "Z.compare" ≔ Z.{|≐|};

rocq/mapping.v

@@ -0,0 +1,66 @@
+From Stdlib Require Export Classical_Prop.
+From Stdlib Require Export ClassicalEpsilon.
+
+(* 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).
+
+(* Bool.lp*)
+Definition bool' := {| type := bool ; el := true|}.
+Canonical bool'.
+
+Definition if' (b : bool) {a : Type'} (e1 : a) (e2 : a) := 
+    if b then e1 else e2.
+
+(* Comp.lp*)
+Definition comparison' := {| type := comparison ; el := Eq|}.
+
+Definition isEq (c : comparison) := 
+ match c with
+ | Eq => true
+ | _ => false
+ end.
+
+Definition isLt (c : comparison) := 
+ match c with
+ | Lt => true
+ | _ => false
+ end.	
+
+Definition isGt (c : comparison) := 
+ match c with
+ | Gt => true
+ | _ => false
+ end.		       
+
+Definition case_Comp := fun (A : Type') (c : comparison') (x y z : A) =>
+match c with
+| Eq => x
+| Lt => y
+| Gt => z
+end.
+
+(* Epsilon.v*)
+ Definition eps : forall {A : Type'}, (type A -> Prop) -> type A :=
+  fun A P => epsilon (inhabits (el A)) P.
+
+Lemma eps_spec {A : Type'} {P : type A -> Prop} : (exists x, P x) -> P (eps P).
+Proof. intro h. unfold eps. apply epsilon_spec. exact h. Qed.
+
+

rocq/renaming.lp

@@ -0,0 +1,21 @@
+// Classic
+builtin "not_not_elim" ≔ {|¬¬ₑ|};
+builtin "or_not_intro" ≔ {|∨¬ᵢ|};
+builtin "ex_not_intro" ≔ {|∃¬ᵢ|};
+
+// Bool
+builtin "ind_bool" ≔ {|ind_𝔹|};
+builtin "case_bool" ≔ {|case_𝔹|};
+builtin "ind_bool_eq" ≔ {|ind_𝔹_eq|};
+
+// Nat
+builtin "geb" ≔ {|≥|};
+builtin "gtb" ≔ >;
+builtin "exp" ≔ ^;
+builtin "factorial" ≔ !;
+
+// List
+builtin "In_nat" ≔ {|∈ₙ|};
+builtin "is_nil" ≔ {|is□|};
+builtin "incl" ≔ {|⊆|};
+builtin "incl_nat" ≔ {|⊆ₙ|};