From e881c5b453b4ed04b2f00edf36d360407e4fa05c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Sat, 3 Oct 2026 16:48:48 +0200 Subject: [PATCH] update --- Bool.lp | 2 +- Comp.lp | 4 +--- Conj.lp | 7 +++---- Coprod.lp | 2 +- DepProd.lp | 12 +++++------- Disj.lp | 7 +++---- Epsilon.lp | 2 ++ ExtraRules.lp | 2 +- FOL.lp | 2 +- HOL.lp | 2 ++ Impred.lp | 2 ++ List.lp | 3 ++- NaryFun.lp | 3 ++- Nat.lp | 3 ++- Pos.lp | 3 ++- Prod.lp | 2 +- Prop.lp | 2 +- PropExt.lp | 2 ++ Quotient.lp | 5 ++--- QuotientExample.lp | 6 +++--- README.md | 46 ++++++++++++++++++++++++++++++++-------------- Set.lp | 2 +- String.lp | 2 +- Subset.lp | 2 +- Tactic.lp | 2 +- Univ.lp | 2 ++ Z.lp | 3 ++- summary | 6 ++++++ 28 files changed, 85 insertions(+), 53 deletions(-) create mode 100755 summary diff --git a/Bool.lp b/Bool.lp index f69aa25..8b5afc4 100644 --- a/Bool.lp +++ b/Bool.lp @@ -1,4 +1,4 @@ -/* Library on booleans. */ +// booleans require open Stdlib.FOL Stdlib.Eq; diff --git a/Comp.lp b/Comp.lp index 100baaa..d8731ba 100644 --- a/Comp.lp +++ b/Comp.lp @@ -1,6 +1,4 @@ -/* Comparison datatype - -By Quentin Garchery (May 2021). */ +// comparison datatype require open Stdlib.Bool; diff --git a/Conj.lp b/Conj.lp index 75e017a..f5c0aab 100644 --- a/Conj.lp +++ b/Conj.lp @@ -1,7 +1,6 @@ -/* Library on Meta-Theorems for Conjunctions - -------------------- +// varyadic conjunction +/* The library proves the following meta-theorems: ** n-ary Natural Deduction rules: @@ -122,4 +121,4 @@ begin have ConjImpCl : π (conj cnf ⇒ clause cnf id) {refine h0 cnf (indexes_decrement id x cnf h2)}; refine clause_ext cnf x id (ConjImpCl (conj_tail x cnf h3))}} -end; \ No newline at end of file +end; diff --git a/Coprod.lp b/Coprod.lp index a2ad23f..59bab06 100644 --- a/Coprod.lp +++ b/Coprod.lp @@ -1,4 +1,4 @@ -// Co-Cartesian product (disjoint sum) +// disjoint sum require open Stdlib.FOL Stdlib.Eq; diff --git a/DepProd.lp b/DepProd.lp index 722c8a4..37afaca 100644 --- a/DepProd.lp +++ b/DepProd.lp @@ -1,4 +1,4 @@ -// Dependent product: a dependent pair of an element and an element in Set +// dependent pairs require open Stdlib.Eq; @@ -9,11 +9,11 @@ constant symbol dprod [a: Set] : (τ a → Set) → Set; rule τ (@dprod $a $p) ↪ @DProd $a $p; -symbol proj₁ [a] [p] (e: @DProd a p) : τ a; +symbol proj₁ [a p] (e: @DProd a p) : τ a; rule proj₁ (dpair $x _) ↪ $x; -symbol proj₂ [a] [p] (e: @DProd a p) : τ (p (proj₁ e)); +symbol proj₂ [a p] (e: @DProd a p) : τ (p (proj₁ e)); rule proj₂ (dpair _ $u) ↪ $u; @@ -23,13 +23,11 @@ begin assume a p; induction; reflexivity end; opaque symbol eq_proj₁ [a] [p] (x y: @DProd a p) : π (x = y) → π (proj₁ x = proj₁ y) ≔ -begin assume a p x y h; refine feq (λ e, proj₁ e) h end; +begin assume a p x y h; refine feq proj₁ h end; opaque symbol eq_dpair_refl [a] [p] (x: τ a) (u v: τ (p x)) : π (u = v) → π (@dpair a p x u = dpair x v) ≔ -begin - assume a p x u v h; refine feq (λ w, @dpair a p x w) h -end; +begin assume a p x u v h; refine feq (dpair x) h end; symbol transport [a] (p: τ a → Set) [x y: τ a] : π (x = y) → τ (p x) → τ (p y); rule transport _ (eq_refl _) $u ↪ $u; diff --git a/Disj.lp b/Disj.lp index 6497185..e0ada6b 100644 --- a/Disj.lp +++ b/Disj.lp @@ -1,7 +1,6 @@ -/* Library on Meta-Theorems for Disjunctions - -------------------- +// varyadic disjunction +/* The library proves the following meta-theorems: ** n-ary Natural Deduction rules: @@ -400,4 +399,4 @@ begin end; assert l0 l1 l2 l2' ⊢ transform [l2'] (l0 ⸬ l1 ⸬ l2 ⸬ l1 ⸬ □) 2 : - (π l2 → π l2') → π (l0 ∨ l1 ∨ l2 ∨ l1) → π (l0 ∨ l1 ∨ l2' ∨ l1); \ No newline at end of file + (π l2 → π l2') → π (l0 ∨ l1 ∨ l2 ∨ l1) → π (l0 ∨ l1 ∨ l2' ∨ l1); diff --git a/Epsilon.lp b/Epsilon.lp index 462536d..e25d0c7 100644 --- a/Epsilon.lp +++ b/Epsilon.lp @@ -1,3 +1,5 @@ +// Hilbert choice operator + require open Stdlib.FOL; symbol ε [a:Set] : (τ a → Prop) → τ a; diff --git a/ExtraRules.lp b/ExtraRules.lp index b3461c3..a9ee0a7 100644 --- a/ExtraRules.lp +++ b/ExtraRules.lp @@ -1,4 +1,4 @@ -// This module turns proved equalities to rewrite rules +// additional rewrite rules derived from proved equalities // Bool diff --git a/FOL.lp b/FOL.lp index 865568a..e48600f 100644 --- a/FOL.lp +++ b/FOL.lp @@ -1,4 +1,4 @@ -// (multi-sorted) First-order logic +// polymorphic first-order logic require open Stdlib.Set Stdlib.Prop; diff --git a/HOL.lp b/HOL.lp index 08dd3bf..cb38972 100644 --- a/HOL.lp +++ b/HOL.lp @@ -1,3 +1,5 @@ +// higher-order logic + require open Stdlib.Set; constant symbol ⤳ : Set → Set → Set; // \leadsto diff --git a/Impred.lp b/Impred.lp index 38b5eb3..3920f0e 100644 --- a/Impred.lp +++ b/Impred.lp @@ -1,3 +1,5 @@ +// impredicativity (quantification on propositions) + require open Stdlib.Set Stdlib.Prop; symbol o : Set; diff --git a/List.lp b/List.lp index 6e4a161..5ceba6c 100644 --- a/List.lp +++ b/List.lp @@ -1,5 +1,6 @@ -/* Library on polymorphic lists +// polymorphic lists +/* following https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v seq.v documentation diff --git a/NaryFun.lp b/NaryFun.lp index 69c7522..231928c 100644 --- a/NaryFun.lp +++ b/NaryFun.lp @@ -1,5 +1,6 @@ -/* n-ary functions and relations +// n-ary functions and relations +/* following "Generic Level Polymorphic N-ary Functions" by Guillaume Allais (TyDe 2019). */ diff --git a/Nat.lp b/Nat.lp index db78b0e..0f49d93 100644 --- a/Nat.lp +++ b/Nat.lp @@ -1,5 +1,6 @@ -/* Library on natural numbers +// unary natural numbers +/* following https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v Documentation of ssrnat.v diff --git a/Pos.lp b/Pos.lp index 0cb0165..8114ab3 100644 --- a/Pos.lp +++ b/Pos.lp @@ -1,5 +1,6 @@ -// Positive binary integers following Rocq stdlib +// positive binary integers +// following Rocq stdlib require open Stdlib.Nat Stdlib.Comp; inductive ℙ : TYPE ≔ diff --git a/Prod.lp b/Prod.lp index af2a3c3..c1ff2f8 100644 --- a/Prod.lp +++ b/Prod.lp @@ -58,7 +58,7 @@ begin reflexivity end; symbol prodExt [a b] (x: τ (a × b)) : π (x = (x ₁) ‚ (x ₂)) ≔ begin - assume a; refine ind_Prod a (λ b x, x = (x ₁) ‚ (x ₂)) _; reflexivity + assume a b; refine ind_Prod (λ x, x = (x ₁) ‚ (x ₂)) _; reflexivity end; opaque symbol eq_pair [a b] (x y: τ (a × b)) : diff --git a/Prop.lp b/Prop.lp index a9adf96..9a6ef8a 100644 --- a/Prop.lp +++ b/Prop.lp @@ -1,4 +1,4 @@ -// Propositional logic +// propositional logic constant symbol Prop : TYPE; diff --git a/PropExt.lp b/PropExt.lp index 8830268..baa28f4 100644 --- a/PropExt.lp +++ b/PropExt.lp @@ -1,3 +1,5 @@ +// propositional extensionality + /*************************************************************************** This file provides an axiom and various theorems for propositional equality. The theorems are grouped into sections by theme: diff --git a/Quotient.lp b/Quotient.lp index 3c5dfb7..e9a2bbd 100644 --- a/Quotient.lp +++ b/Quotient.lp @@ -1,4 +1,4 @@ -// Quotient types +// quotient types require open Stdlib.Eq; @@ -12,7 +12,6 @@ notation ⫽ infix 30; rule τ (_ ⫽ $R) ↪ Quot $R; symbol class [a] r ≔ @cl a r; -symbol ind_quot [a] ≔ ind_Quot a; symbol sound [a] (r:Rel a) x y: π(r x y) → π (class r x = class r y); @@ -31,7 +30,7 @@ begin { assume x x' xx'; set p ≔ λ x y y' yy', hf x x (hr x) y y' yy'; change π(lift r (f x) (p x) d = lift r (f x') (p x') d); set q ≔ λ d, lift r (f x) (p x) d = lift r (f x') (p x') d; - change π(q d); apply ind_quot r q _ d; + change π(q d); apply ind_Quot q _ d; assume y; simplify; apply hf {apply xx'} {apply hr} } end; diff --git a/QuotientExample.lp b/QuotientExample.lp index b7fa1e0..b2e8c69 100644 --- a/QuotientExample.lp +++ b/QuotientExample.lp @@ -1,4 +1,4 @@ -// example of quotient: integers +// example of quotient type require open Stdlib.Nat Stdlib.Prod Stdlib.Quotient; @@ -38,7 +38,7 @@ require open Stdlib.FOL; opaque symbol +_com a b: π (+ a b = + b a) ≔ begin - refine ind_quot intrel (λ a, `∀ b, + a b = + b a) _; assume x; - refine ind_quot intrel (λ b, + (class intrel x) b = + b (class intrel x)) _; assume y; + refine ind_Quot (λ a, `∀ b, + a b = + b a) _; assume x; + refine ind_Quot (λ b, + (class intrel x) b = + b (class intrel x)) _; assume y; apply sound; simplify; rewrite addnC (x ₁); rewrite addnC (y ₂); reflexivity end; diff --git a/README.md b/README.md index 02bfa5f..4cabc2b 100644 --- a/README.md +++ b/README.md @@ -1,28 +1,46 @@ Standard library of [Lambdapi](https://github.com/Deducteam/lambdapi) ===================================================================== -- `Prop`: propositional logic -- `Eq`: equality -- `Set`: set codes for polymorphism -- `FOL`: typed first-order logic - `Bool`: booleans -- `Nat`: natural numbers -- `List`: polymorphic lists - `Classic`: classical logic +- `Comp`: comparison datatype +- `Conj`: varyadic conjunction +- `Coprod`: disjoint sum +- `DepProd`: dependent pairs +- `Disj`: varyadic disjunction +- `Epsilon`: Hilbert choice operator +- `Eq`: polymorphic Leibniz equality +- `ExtraRules`: additional rewrite rules derived from proved equalities +- `FOL`: polymorphic first-order logic +- `FunExt`: require open Stdlib.Eq Stdlib.HOL; +- `HOL`: higher-order logic +- `Impred`: impredicativity (quantification on propositions) +- `List`: polymorphic lists +- `NaryFun`: n-ary functions and relations +- `Nat`: unary natural numbers +- `Option`: option type +- `Pos`: positive binary integers +- `Prod`: Cartesian product +- `PropExt`: propositional extensionality +- `Prop`: propositional logic +- `QuotientExample`: example of quotient type +- `Quotient`: quotient types +- `Set`: type of type codes +- `String`: builtin string type +- `Subset`: subset types +- `Tactic`: tactic type +- `Univ`: universes +- `Z`: binary integers The libraries on natural numbers and polymorphic lists follow the -corresponding Coq SSReflect libraries: - -- [ssrnat.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v) - -- [seq.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v) +corresponding Rocq SSReflect libraries [ssrnat.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnat.v) +and [seq.v](https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/seq.v). The library on integers follow the one of the Rocq standard library. Installation with Opam ---------------------- ``` -opam repository -a --set-default add lambdapi https://github.com/deducteam/opam-lambdapi-repos -itory.git # once +opam repository -a --set-default add lambdapi https://github.com/deducteam/opam-lambdapi-repository.git # once opam install lambdapi-stdlib ``` @@ -30,7 +48,7 @@ Usage in Lambdapi ----------------- ``` -require open Stdlib.Prop Stdlib.Set Stdlib.FOL Stdlib.Nat /* ... */; +require open Stdlib.Nat; ``` Compilation from the sources diff --git a/Set.lp b/Set.lp index 81d1758..1adc70f 100644 --- a/Set.lp +++ b/Set.lp @@ -1,4 +1,4 @@ -// Type of set codes for quantifying over sets (polymorphism) +// type of type codes constant symbol Set : TYPE; diff --git a/String.lp b/String.lp index 936ccce..d8751d7 100644 --- a/String.lp +++ b/String.lp @@ -1,4 +1,4 @@ -// builtin type of strings +// builtin string type require open Stdlib.Set; diff --git a/Subset.lp b/Subset.lp index 300fab9..485c880 100644 --- a/Subset.lp +++ b/Subset.lp @@ -1,4 +1,4 @@ -// Subset types: a dependent pair of an element and a proof +// subset types require open Stdlib.FOL Stdlib.Eq; diff --git a/Tactic.lp b/Tactic.lp index 2b37519..4faa389 100644 --- a/Tactic.lp +++ b/Tactic.lp @@ -1,4 +1,4 @@ -// define a type representing Lambdapi tactics +// tactic type require open Stdlib.String Stdlib.Univ; diff --git a/Univ.lp b/Univ.lp index 1b76885..8c6fbb4 100644 --- a/Univ.lp +++ b/Univ.lp @@ -1,3 +1,5 @@ +// universes + require open Stdlib.Set Stdlib.Prop; constant symbol L:TYPE; diff --git a/Z.lp b/Z.lp index 4550574..a4d8b1d 100644 --- a/Z.lp +++ b/Z.lp @@ -1,5 +1,6 @@ -// Binary integers (following Rocq stdlib) +// binary integers +// following Rocq stdlib require open Stdlib.Pos; inductive ℤ : TYPE ≔ // \BbbZ diff --git a/summary b/summary new file mode 100755 index 0000000..df54a7c --- /dev/null +++ b/summary @@ -0,0 +1,6 @@ +#!/bin/sh + +for f in `ls *.lp` +do + echo "- \`${f%.lp}\`: `head -n1 $f | sed -e 's/^\/\/ //'`" +done