diff --git a/rocq/.gitignore b/rocq/.gitignore new file mode 100644 index 0000000..3f7fde5 --- /dev/null +++ b/rocq/.gitignore @@ -0,0 +1,11 @@ +.*.aux +*.v +!mappings.v +*.vo* +*.glob +rocq.mk +rocq.mk.conf +.rocq.mk.d +*.dk* +dko.mk + diff --git a/rocq/Makefile b/rocq/Makefile new file mode 100644 index 0000000..18e5713 --- /dev/null +++ b/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 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..1ff7bed --- /dev/null +++ b/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" ≔ {|¬|}; diff --git a/rocq/mapping.lp b/rocq/mapping.lp new file mode 100644 index 0000000..20249ba --- /dev/null +++ b/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.{|≐|}; diff --git a/rocq/mapping.v b/rocq/mapping.v new file mode 100644 index 0000000..79c8204 --- /dev/null +++ b/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. + + diff --git a/rocq/renaming.lp b/rocq/renaming.lp new file mode 100644 index 0000000..db5bac6 --- /dev/null +++ b/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" ≔ {|⊆ₙ|};