From 152676cb1c8f12e206ca82b90c4b82791b45b92e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Tue, 25 Nov 2025 11:32:57 +0100 Subject: [PATCH 1/5] 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). From d07896d3612c9eab80e0893192cb2dbd205ce87d Mon Sep 17 00:00:00 2001 From: Catherine Date: Tue, 25 Nov 2025 17:04:16 +0100 Subject: [PATCH 2/5] Done jusque Fun exclus --- rocq/mappings.lp | 29 ++++++++++++++++++++++++++++- rocq/mappings.v | 47 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 75 insertions(+), 1 deletion(-) diff --git a/rocq/mappings.lp b/rocq/mappings.lp index 2230297..221ac35 100644 --- a/rocq/mappings.lp +++ b/rocq/mappings.lp @@ -10,7 +10,7 @@ builtin "and" ≔ ∧; builtin "conj" ≔ ∧ᵢ; builtin "proj1" ≔ ∧ₑ₁; builtin "proj2" ≔ ∧ₑ₂; -builtin "or" ≔ ∨; +builtin "\/" ≔ ∨; builtin "or_intro1" ≔ ∨ᵢ₁; builtin "or_intro2" ≔ ∨ᵢ₂; builtin "or_elim" ≔ ∨ₑ; @@ -29,8 +29,35 @@ builtin "ex" ≔ ∃; // HOL.lp builtin "arr" ≔ ⤳; + // Eq.lp builtin "eq" ≔ =; builtin "eq_refl" ≔ eq_refl; builtin "ind_eq" ≔ ind_eq; builtin "neq" ≔ ≠; + +//Bool.lp +builtin "bool'" ≔ 𝔹; +builtin "bool'" ≔ bool; +builtin "Is_true" ≔ istrue; +builtin "negb" ≔ not; +builtin "orb" ≔ or; +builtin "andb" ≔ and; +builtin "if'" ≔ if; + +//Classic.lp +builtin "classic" ≔ em; + +//Comp.lp +builtin "comparison'" ≔ comp; +builtin "comparison'" ≔ Comp; +builtin "CompOpp" ≔ opp; +builtin "isEq" ≔ isEq; +builtin "isLt" ≔ isLt; +builtin "isGT" ≔ isGT; +builtin "case_Comp" ≔ case_Comp; + +//Epsilon.lp +builtin "eps" ≔ ε; +builtin "eps_spec" ≔ εᵢ; + diff --git a/rocq/mappings.v b/rocq/mappings.v index 2f541f2..79c8204 100644 --- a/rocq/mappings.v +++ b/rocq/mappings.v @@ -1,3 +1,6 @@ +From Stdlib Require Export Classical_Prop. +From Stdlib Require Export ClassicalEpsilon. + (* Prop.lp *) Definition imp (p q : Prop) : Prop := p -> q. @@ -17,3 +20,47 @@ 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. + + From 40a1618a27d87886961c6f926ad5332bc96f7795 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 18 Jun 2026 13:30:45 +0200 Subject: [PATCH 3/5] wip --- rocq/Makefile | 19 +++++++++++++++---- rocq/mappings.lp | 30 +++++++++++++++++++++--------- rocq/renaming.lp | 5 +++++ 3 files changed, 41 insertions(+), 13 deletions(-) create mode 100644 rocq/renaming.lp diff --git a/rocq/Makefile b/rocq/Makefile index f613a80..539425b 100644 --- a/rocq/Makefile +++ b/rocq/Makefile @@ -2,21 +2,32 @@ LPFILES := $(wildcard ../*.lp) VFILES := $(LPFILES:../%.lp=%.v) VOFILES := $(VFILES:%=%o) -default: v +.PHONY: default +default: + $(MAKE) v + $(MAKE) vo +.PHONY: 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)" + lambdapi export -o stt_coq --encoding encoding.lp --renaming renaming.lp --mapping mappings.lp --requiring mappings --use-notations ../$*.lp > $@ -clean-v: +.PHONY: clean-v +clean-v: clean-vo rm -f $(VFILES) rocq.mk: _CoqProject rocq makefile -f _CoqProject -o $@ +.PHONY: vo vo: rocq.mk $(MAKE) -f rocq.mk +.PHONY: clean-vo clean-vo: - rm -f $(VOFILES) + rm -f *.vo* + +.PHONY: clean +clean: clean-v + rm -f rocq.mk rocq.mk.conf *.glob diff --git a/rocq/mappings.lp b/rocq/mappings.lp index 221ac35..b359710 100644 --- a/rocq/mappings.lp +++ b/rocq/mappings.lp @@ -1,4 +1,4 @@ -// Prop.lp +// Prop builtin "Prop" ≔ Prop; builtin "True" ≔ ⊤; builtin "I" ≔ ⊤ᵢ; @@ -18,25 +18,28 @@ builtin "ex_intro" ≔ ∃ᵢ; builtin "ex_elim" ≔ ∃ₑ; builtin "iff" ≔ ⇔; -// Set.lp +// Set builtin "Type'" ≔ Set; builtin "nat" ≔ ι; builtin "el" ≔ el; -// FOL.lp +// Prod +builtin "prod" ≔ ×; + +// FOL builtin "all" ≔ ∀; builtin "ex" ≔ ∃; -// HOL.lp +// HOL builtin "arr" ≔ ⤳; -// Eq.lp +// Eq builtin "eq" ≔ =; builtin "eq_refl" ≔ eq_refl; builtin "ind_eq" ≔ ind_eq; builtin "neq" ≔ ≠; -//Bool.lp +// Bool builtin "bool'" ≔ 𝔹; builtin "bool'" ≔ bool; builtin "Is_true" ≔ istrue; @@ -45,10 +48,10 @@ builtin "orb" ≔ or; builtin "andb" ≔ and; builtin "if'" ≔ if; -//Classic.lp +// Classic builtin "classic" ≔ em; -//Comp.lp +// Comp builtin "comparison'" ≔ comp; builtin "comparison'" ≔ Comp; builtin "CompOpp" ≔ opp; @@ -57,7 +60,16 @@ builtin "isLt" ≔ isLt; builtin "isGT" ≔ isGT; builtin "case_Comp" ≔ case_Comp; -//Epsilon.lp +// Epsilon builtin "eps" ≔ ε; builtin "eps_spec" ≔ εᵢ; +// Nat +builtin "nat" ≔ ℕ; + +// List +builtin "List" ≔ 𝕃; +builtin "nil" ≔ □; +builtin "cons" ≔ ⸬; +builtin "List.In" ≔ ∈; +builtin "app" ≔ ++; diff --git a/rocq/renaming.lp b/rocq/renaming.lp new file mode 100644 index 0000000..739755c --- /dev/null +++ b/rocq/renaming.lp @@ -0,0 +1,5 @@ +// List +builtin "In_nat" ≔ ∈ₙ; +builtin "is_nil" ≔ is□; +builtin "incl" ≔ ⊆; +builtin "incl_nat" ≔ ⊆ₙ; From 69602598e2539cfe060d79d94e8af16731073281 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 18 Jun 2026 18:29:11 +0200 Subject: [PATCH 4/5] wip --- rocq/mappings.lp | 53 ++++++++++++++++++++++++++++++++++++++++++++++-- rocq/renaming.lp | 6 ++++++ 2 files changed, 57 insertions(+), 2 deletions(-) diff --git a/rocq/mappings.lp b/rocq/mappings.lp index b359710..b5cc0e4 100644 --- a/rocq/mappings.lp +++ b/rocq/mappings.lp @@ -25,6 +25,9 @@ builtin "el" ≔ el; // Prod builtin "prod" ≔ ×; +builtin "pair" ≔ ‚; +builtin "fst" ≔ ₁; +builtin "snd" ≔ ₂; // FOL builtin "all" ≔ ∀; @@ -61,11 +64,19 @@ builtin "isGT" ≔ isGT; builtin "case_Comp" ≔ case_Comp; // Epsilon -builtin "eps" ≔ ε; -builtin "eps_spec" ≔ εᵢ; +builtin "eps" ≔ ε; +builtin "eps_spec" ≔ εᵢ; // Nat builtin "nat" ≔ ℕ; +builtin "O" ≔ _0; +builtin "S" ≔ +1; +builtin "Nat.add" ≔ +; +builtin "Nat.sub" ≔ -; +builtin "Nat.pred" ≔ ∸1; +builtin "Nat.mul" ≔ *; +builtin "Nat.leb" ≔ ≤; +builtin "Nat.ltb" ≔ <; // List builtin "List" ≔ 𝕃; @@ -73,3 +84,41 @@ builtin "nil" ≔ □; builtin "cons" ≔ ⸬; builtin "List.In" ≔ ∈; builtin "app" ≔ ++; + +// Pos +builtin "positive" ≔ ℙ; +builtin "xI" ≔ I; +builtin "xO" ≔ O; +builtin "xH" ≔ H; + +// Z +builtin "Z" ≔ ℤ; +builtin "Z0" ≔ Z0; +builtin "Zpos" ≔ Zpos; +builtin "Zneg" ≔ Zneg; +builtin "Z.opp" ≔ —; +builtin "Z.compare" ≔ ≐; + +// Tactic +builtin "(*#admit*)" ≔ #admit; +builtin "(*&*)" ≔ &; +builtin "(*#apply*)" ≔ #apply; +builtin "(*#assume*)" ≔ #assume; +builtin "(*#fail*)" ≔ #fail; +builtin "(*#generalize*)" ≔ #generalize; +builtin "(*#have*)" ≔ #have; +builtin "(*#induction*)" ≔ #induction; +builtin "(*#orelse*)" ≔ #orelse; +builtin "(*#refine*)" ≔ #refine; +builtin "(*#reflexivity*)" ≔ #reflexivity; +builtin "(*#remove*)" ≔ #remove; +builtin "(*#repeat*)" ≔ #repeat; +builtin "(*#rewrite*)" ≔ #rewrite; +builtin "(*#set*)" ≔ #set; +builtin "(*#simplify*)" ≔ #simplify; +builtin "(*#simplify_beta*)" ≔ #simplify_beta; +builtin "(*#solve*)" ≔ #solve; +builtin "(*#symetry*)" ≔ #symmetry; +builtin "(*#try*)" ≔ #try; +builtin "(*#why3*)" ≔ #why3; +builtin "(*#change*)" ≔ #change; diff --git a/rocq/renaming.lp b/rocq/renaming.lp index 739755c..7aa9530 100644 --- a/rocq/renaming.lp +++ b/rocq/renaming.lp @@ -1,3 +1,9 @@ +// Nat +builtin "geb" ≔ ≥; +builtin "gtb" ≔ >; +builtin "exp" ≔ ^; +builtin "factorial" ≔ !; + // List builtin "In_nat" ≔ ∈ₙ; builtin "is_nil" ≔ is□; From f0ae0f76ba28656f4e353fb746cbfbfe06fff179 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 18 Jun 2026 19:39:35 +0200 Subject: [PATCH 5/5] wip --- rocq/.gitignore | 3 + rocq/Makefile | 44 +++++++++--- rocq/encoding.lp | 21 +++--- rocq/mapping.lp | 100 ++++++++++++++++++++++++++ rocq/{mappings.v => mapping.v} | 0 rocq/mappings.lp | 124 --------------------------------- rocq/renaming.lp | 20 ++++-- 7 files changed, 164 insertions(+), 148 deletions(-) create mode 100644 rocq/mapping.lp rename rocq/{mappings.v => mapping.v} (100%) delete mode 100644 rocq/mappings.lp diff --git a/rocq/.gitignore b/rocq/.gitignore index e673e3d..3f7fde5 100644 --- a/rocq/.gitignore +++ b/rocq/.gitignore @@ -6,3 +6,6 @@ rocq.mk rocq.mk.conf .rocq.mk.d +*.dk* +dko.mk + diff --git a/rocq/Makefile b/rocq/Makefile index 539425b..18e5713 100644 --- a/rocq/Makefile +++ b/rocq/Makefile @@ -1,21 +1,50 @@ -LPFILES := $(wildcard ../*.lp) -VFILES := $(LPFILES:../%.lp=%.v) -VOFILES := $(VFILES:%=%o) +.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 mappings.lp ../%.lp - lambdapi export -o stt_coq --encoding encoding.lp --renaming renaming.lp --mapping mappings.lp --requiring mappings --use-notations ../$*.lp > $@ +%.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) + -rm -f $(VFILES) rocq.mk rocq.mk.conf *.glob rocq.mk: _CoqProject rocq makefile -f _CoqProject -o $@ @@ -29,5 +58,4 @@ clean-vo: rm -f *.vo* .PHONY: clean -clean: clean-v - rm -f rocq.mk rocq.mk.conf *.glob +clean: clean-dk diff --git a/rocq/encoding.lp b/rocq/encoding.lp index 5ea7874..1ff7bed 100644 --- a/rocq/encoding.lp +++ b/rocq/encoding.lp @@ -1,16 +1,15 @@ -// dk/lp symbols used for encoding simple type theory +// symbols used for encoding simple type theory -builtin "El" ≔ τ; -builtin "Prf" ≔ π; +builtin "El" ≔ {|τ|}; +builtin "Prf" ≔ {|π|}; -// symbols with special notations in Coq builtin "Set" ≔ Set; builtin "prop" ≔ Prop; -builtin "arr" ≔ ⤳; -builtin "imp" ≔ ⇒; -builtin "all" ≔ ∀; +builtin "arr" ≔ {|⤳|}; +builtin "imp" ≔ {|⇒|}; +builtin "all" ≔ {|∀|}; builtin "eq" ≔ =; -builtin "or" ≔ ∨; -builtin "and" ≔ ∧; -builtin "ex" ≔ ∃; -builtin "not" ≔ ¬; +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/mappings.v b/rocq/mapping.v similarity index 100% rename from rocq/mappings.v rename to rocq/mapping.v diff --git a/rocq/mappings.lp b/rocq/mappings.lp deleted file mode 100644 index b5cc0e4..0000000 --- a/rocq/mappings.lp +++ /dev/null @@ -1,124 +0,0 @@ -// Prop -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 "\/" ≔ ∨; -builtin "or_intro1" ≔ ∨ᵢ₁; -builtin "or_intro2" ≔ ∨ᵢ₂; -builtin "or_elim" ≔ ∨ₑ; -builtin "ex_intro" ≔ ∃ᵢ; -builtin "ex_elim" ≔ ∃ₑ; -builtin "iff" ≔ ⇔; - -// Set -builtin "Type'" ≔ Set; -builtin "nat" ≔ ι; -builtin "el" ≔ el; - -// Prod -builtin "prod" ≔ ×; -builtin "pair" ≔ ‚; -builtin "fst" ≔ ₁; -builtin "snd" ≔ ₂; - -// FOL -builtin "all" ≔ ∀; -builtin "ex" ≔ ∃; - -// HOL -builtin "arr" ≔ ⤳; - -// Eq -builtin "eq" ≔ =; -builtin "eq_refl" ≔ eq_refl; -builtin "ind_eq" ≔ ind_eq; -builtin "neq" ≔ ≠; - -// Bool -builtin "bool'" ≔ 𝔹; -builtin "bool'" ≔ bool; -builtin "Is_true" ≔ istrue; -builtin "negb" ≔ not; -builtin "orb" ≔ or; -builtin "andb" ≔ and; -builtin "if'" ≔ if; - -// Classic -builtin "classic" ≔ em; - -// Comp -builtin "comparison'" ≔ comp; -builtin "comparison'" ≔ Comp; -builtin "CompOpp" ≔ opp; -builtin "isEq" ≔ isEq; -builtin "isLt" ≔ isLt; -builtin "isGT" ≔ isGT; -builtin "case_Comp" ≔ case_Comp; - -// Epsilon -builtin "eps" ≔ ε; -builtin "eps_spec" ≔ εᵢ; - -// Nat -builtin "nat" ≔ ℕ; -builtin "O" ≔ _0; -builtin "S" ≔ +1; -builtin "Nat.add" ≔ +; -builtin "Nat.sub" ≔ -; -builtin "Nat.pred" ≔ ∸1; -builtin "Nat.mul" ≔ *; -builtin "Nat.leb" ≔ ≤; -builtin "Nat.ltb" ≔ <; - -// List -builtin "List" ≔ 𝕃; -builtin "nil" ≔ □; -builtin "cons" ≔ ⸬; -builtin "List.In" ≔ ∈; -builtin "app" ≔ ++; - -// Pos -builtin "positive" ≔ ℙ; -builtin "xI" ≔ I; -builtin "xO" ≔ O; -builtin "xH" ≔ H; - -// Z -builtin "Z" ≔ ℤ; -builtin "Z0" ≔ Z0; -builtin "Zpos" ≔ Zpos; -builtin "Zneg" ≔ Zneg; -builtin "Z.opp" ≔ —; -builtin "Z.compare" ≔ ≐; - -// Tactic -builtin "(*#admit*)" ≔ #admit; -builtin "(*&*)" ≔ &; -builtin "(*#apply*)" ≔ #apply; -builtin "(*#assume*)" ≔ #assume; -builtin "(*#fail*)" ≔ #fail; -builtin "(*#generalize*)" ≔ #generalize; -builtin "(*#have*)" ≔ #have; -builtin "(*#induction*)" ≔ #induction; -builtin "(*#orelse*)" ≔ #orelse; -builtin "(*#refine*)" ≔ #refine; -builtin "(*#reflexivity*)" ≔ #reflexivity; -builtin "(*#remove*)" ≔ #remove; -builtin "(*#repeat*)" ≔ #repeat; -builtin "(*#rewrite*)" ≔ #rewrite; -builtin "(*#set*)" ≔ #set; -builtin "(*#simplify*)" ≔ #simplify; -builtin "(*#simplify_beta*)" ≔ #simplify_beta; -builtin "(*#solve*)" ≔ #solve; -builtin "(*#symetry*)" ≔ #symmetry; -builtin "(*#try*)" ≔ #try; -builtin "(*#why3*)" ≔ #why3; -builtin "(*#change*)" ≔ #change; diff --git a/rocq/renaming.lp b/rocq/renaming.lp index 7aa9530..db5bac6 100644 --- a/rocq/renaming.lp +++ b/rocq/renaming.lp @@ -1,11 +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 "geb" ≔ {|≥|}; builtin "gtb" ≔ >; builtin "exp" ≔ ^; builtin "factorial" ≔ !; // List -builtin "In_nat" ≔ ∈ₙ; -builtin "is_nil" ≔ is□; -builtin "incl" ≔ ⊆; -builtin "incl_nat" ≔ ⊆ₙ; +builtin "In_nat" ≔ {|∈ₙ|}; +builtin "is_nil" ≔ {|is□|}; +builtin "incl" ≔ {|⊆|}; +builtin "incl_nat" ≔ {|⊆ₙ|};