From 1f5889fe1073fd4c41884ea808ffe05cbbd7ef16 Mon Sep 17 00:00:00 2001 From: NotBad4U Date: Thu, 17 Sep 2026 01:42:29 +0200 Subject: [PATCH 1/6] Add interfaces to declare generic level polymorphic n-ary functions This work is based on Guillaume Allais - "Generic Level Polymorphic N-ary Functions" (TyDe 2019) --- HOL.lp | 5 ++ NaryFunctions.lp | 143 +++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 148 insertions(+) create mode 100644 NaryFunctions.lp diff --git a/HOL.lp b/HOL.lp index f5e4ac6..11b529b 100644 --- a/HOL.lp +++ b/HOL.lp @@ -13,3 +13,8 @@ notation ⤳d infix right 20; rule $a ⤳d λ _,$b.[] ↪ $a ⤳ $b; rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x]; + +// function composition +symbol ∘ [a b c] : τ (b ⤳ c) → τ (a ⤳ b) → τ a → τ c ≔ λ g f x, g (f x); + +notation ∘ infix 20; \ No newline at end of file diff --git a/NaryFunctions.lp b/NaryFunctions.lp new file mode 100644 index 0000000..845f8a9 --- /dev/null +++ b/NaryFunctions.lp @@ -0,0 +1,143 @@ +// Implementation of N-ary functions and relations based on Guillaume Allais, +// "Generic Level Polymorphic N-ary Functions" (TyDe 2019). +// This API provides n-ary functions which automatically reconstruct the representation of their inputs' types by unification. +// It helps to define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families, +// that are used by programs such as SMT solvers. Lemmas provided in the rest of the library such as `Eq.lp` are implemented for +// fixed arities, and the implementation here aims to provide similar lemmas for N-ary Combinators. + +require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.HOL Stdlib.Nat Stdlib.Eq Stdlib.Impred; + +inductive Sets : ℕ → TYPE ≔ +| Unit : Sets 0 +| ▹ : Π [n : ℕ], Set → Sets n → Sets (n +1); + +notation ▹ infix right 10; + +symbol sets (n : ℕ) : Set; +rule τ (sets $n) ↪ Sets $n; + +// Type transformer x1 ▹ x2 ▹ .. into x1 ⤳ x2 ⤳ .. +symbol arrows n : Sets n → Set → Set; +rule arrows 0 Unit $b ↪ $b +with arrows ($n +1) ($t ▹ $ts) $b ↪ $t ⤳ (arrows $n $ts $b); + +injective symbol Arrow [n] (dom : Sets n) (cod : Set) : TYPE ≔ τ (@arrows n dom cod); + +assert ⊢ Arrow (o ▹ o ▹ Unit) o ≡ (Prop → Prop → Prop); +assert ⊢ (∧) : Arrow (o ▹ o ▹ Unit) o; + +// Tail of a telescope. +symbol tl [n] : Sets (n +1) → Sets n; +rule tl (_ ▹ $ts) ↪ $ts; + + +// The definitions below do not depend on these rules; they only let the `Sets` +// argument stay implicit at use sites such as `congₙ 2 (+)`. +// So the unif rule below allows us to write generic programs acting on n-ary functions +// with less boilerplate. +// Unfolding `arrows` in the unifier. Its rules match on the `Sets` argument, +// so `arrows n ?ts ?b` is stuck when `?ts` is a metavariable: for +// `f : τ A → τ B → τ C` against `Arrow ?ts ?b`, the unifier faces +// `arrows 2 ?ts ?b ≡ A ⤳ B ⤳ C`. The rules below unfold it one step at a +// time, the constructor of `?ts`. +unif_rule @arrows ($n +1) $ts $b ≡ ($a ⤳ $c) ↪ [$ts ≡ @▹ $n $a _; @arrows $n (@tl $n $ts) $b ≡ $c]; +unif_rule @arrows 0 $ts $b ≡ $c ↪ [$ts ≡ Unit; $b ≡ $c]; + +// Helper type constructor to just create an arrow of `n`-times the type `t`. +// Ex: SetsIdent 3 nat ≡ nat ⤳ nat ⤳ nat +symbol SetsIdent n (t : Set) : Sets n; +rule SetsIdent 0 _ ↪ Unit +with SetsIdent ($n +1) $t ↪ $t ▹ (SetsIdent $n $t); + +// Helper type constructor to just create an arrow of `n`-times the type `t`. +// Ex: ArrowI 2 nat ≡ nat ⤳ nat ⤳ nat +symbol ArrowI n (a : Set) ≔ Arrow (SetsIdent n a) a; // Arrow wrapper for SetsIdent + +// ------------------------------------------------------ pointwise liftings + +// Lift a unary operation (τ A → τ B) to n-ary functions. +symbol lift [A B : Set] n [dom : Sets n] : (τ A → τ B) → Arrow dom A → Arrow dom B; +rule @lift _ _ 0 Unit $op $f ↪ $op $f +with @lift $A $B ($n +1) ($t ▹ $ts) $op $f ↪ λ (x : τ $t), @lift $A $B $n $ts $op ($f x); + +// Lift a binary operation to two n-ary functions with the same domain +symbol lift2 [A B C : Set] n [dom : Sets n] : + (τ A → τ B → τ C) → Arrow dom A → Arrow dom B → Arrow dom C; +rule @lift2 _ _ _ 0 Unit $op $f $g ↪ $op $f $g +with @lift2 $A $B $C ($n +1) ($t ▹ $ts) $op $f $g ↪ + λ (x : τ $t), @lift2 $A $B $C $n $ts $op ($f x) ($g x); + +// `composeₙ n g f` precomposes the (n+1)-th argument of g with f: +// composition with f, lifted over the first n arguments. +symbol composeₙ [i j b : Set] n [dom : Sets n] (g : Arrow dom (j ⤳ b)) (f : τ i → τ j) + : Arrow dom (i ⤳ b) ≔ lift n (λ h, h ∘ f) g; + + +symbol ∧ₙ [n] [dom : Sets n] (P Q : Arrow dom o) : Arrow dom o ≔ lift2 n (∧) P Q; + +symbol ∨ₙ [n] [dom : Sets n] (P Q : Arrow dom o) : Arrow dom o ≔ lift2 n (∨) P Q; + +symbol ⇒ₙ [n] [dom : Sets n] (P Q : Arrow dom o) : Arrow dom o ≔ lift2 n (⇒) P Q; + +symbol quantₙ (Q : Π a : Set, (τ a → Prop) → Prop) n [ts : Sets n] : Arrow ts o → Prop; +rule @quantₙ _ 0 Unit $P ↪ $P +with @quantₙ $Q ($n +1) ($t ▹ $ts) $P ↪ $Q $t (λ (x : τ $t), @quantₙ $Q $n $ts ($P x)); + +symbol ∀ₙ n [ts : Sets n] (P : Arrow ts o) : Prop ≔ quantₙ (@∀) n P; +symbol ∃ₙ n [ts : Sets n] (P : Arrow ts o) : Prop ≔ quantₙ (@∃) n P; + +// Cong n f g computes the statement +// `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ f a₁ .. aₙ = g b₁ .. bₙ +symbol Cong n [ts : Sets n] [R : Set] (f g : Arrow ts R) : Prop; +rule @Cong 0 Unit $R $f $g ↪ @= $R $f $g +with @Cong ($n +1) ($t ▹ $ts) $R $f $g ↪ + `∀ (x : τ $t), `∀ (y : τ $t), (x = y) ⇒ @Cong $n $ts $R ($f x) ($g y); + +opaque symbol congₙ [D : Set] n [ts : Sets n] (f : Arrow ts D) : π (@Cong n ts D f f) ≔ +begin + assume D n; + refine ind_Sets (λ n u, `∀ f, @Cong n u D f f) _ _ n + { reflexivity } + { assume m t ts ih; + assume f t1 t2 hrefl; + rewrite hrefl; + refine ih (f t2) } +end; + +// Subst n P Q computes the statement +// `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ P a₁ .. aₙ ⇒ Q b₁ .. bₙ +symbol Subst n [ts : Sets n] (P Q : Arrow ts o) : Prop; +rule @Subst 0 Unit $P $Q ↪ $P ⇒ $Q +with @Subst ($n +1) ($t ▹ $ts) $P $Q ↪ + `∀ (x : τ $t), `∀ (y : τ $t), (x = y) ⇒ @Subst $n $ts ($P x) ($Q y); + +opaque symbol substₙ n [ts : Sets n] (P : Arrow ts o) : π (@Subst n ts P P) ≔ +begin + assume n; + refine ind_Sets (λ n u, `∀ P, @Subst n u P P) _ _ n + { assume P h; refine h } + { assume m t ts ih; + assume P x y hxy; + rewrite hxy; + refine ih (P y) } +end; + +// Examples + +private symbol f1 : Arrow (o ▹ o ▹ o ▹ o ▹ Unit) o; +private symbol f2 : ArrowI 4 o; + +private opaque symbol ex_cong a b c d x y w z : + π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (f1 a b c d = f1 x y w z) ≔ +begin + assume a b c d x y w z heq1 heq2 heq3 heq4; +refine congₙ 4 f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 +end; + +assert (x y : ℕ) + ⊢ let u1 ≔ composeₙ 1 (+) (λ x, x +1) in + u1 x y ≡ x + (y +1); + +private opaque symbol testSubst (P : Arrow (nat ▹ nat ▹ Unit) o) (a b x y : ℕ) : + π (a = x) → π (b = y) → π (P a b) → π (P x y) ≔ +begin assume P a b x y hax hby; refine substₙ 2 P _ _ hax _ _ hby end; \ No newline at end of file From 53e60fa6bbbd604b724988bada8e9ad13ae40152 Mon Sep 17 00:00:00 2001 From: NotBad4U Date: Thu, 17 Sep 2026 23:05:23 +0200 Subject: [PATCH 2/6] Fix comments of PR #73 --- HOL.lp | 2 +- NaryFunctions.lp | 142 +++++++++++++++++++++++------------------------ 2 files changed, 69 insertions(+), 75 deletions(-) diff --git a/HOL.lp b/HOL.lp index 11b529b..662baa6 100644 --- a/HOL.lp +++ b/HOL.lp @@ -17,4 +17,4 @@ rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x]; // function composition symbol ∘ [a b c] : τ (b ⤳ c) → τ (a ⤳ b) → τ a → τ c ≔ λ g f x, g (f x); -notation ∘ infix 20; \ No newline at end of file +notation ∘ infix 20; diff --git a/NaryFunctions.lp b/NaryFunctions.lp index 845f8a9..8e6f6ca 100644 --- a/NaryFunctions.lp +++ b/NaryFunctions.lp @@ -8,7 +8,7 @@ require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.HOL Stdlib.Nat Stdlib.Eq Stdlib.Impred; inductive Sets : ℕ → TYPE ≔ -| Unit : Sets 0 +| unit : Sets 0 | ▹ : Π [n : ℕ], Set → Sets n → Sets (n +1); notation ▹ infix right 10; @@ -17,86 +17,66 @@ symbol sets (n : ℕ) : Set; rule τ (sets $n) ↪ Sets $n; // Type transformer x1 ▹ x2 ▹ .. into x1 ⤳ x2 ⤳ .. -symbol arrows n : Sets n → Set → Set; -rule arrows 0 Unit $b ↪ $b -with arrows ($n +1) ($t ▹ $ts) $b ↪ $t ⤳ (arrows $n $ts $b); +symbol arrows [n] : Sets n → Set → Set; +rule arrows unit $b ↪ $b +with arrows ($t ▹ $ts) $b ↪ $t ⤳ arrows $ts $b; -injective symbol Arrow [n] (dom : Sets n) (cod : Set) : TYPE ≔ τ (@arrows n dom cod); +injective symbol Arrow [n] (dom : Sets n) (cod : Set) : TYPE ≔ τ (arrows dom cod); -assert ⊢ Arrow (o ▹ o ▹ Unit) o ≡ (Prop → Prop → Prop); -assert ⊢ (∧) : Arrow (o ▹ o ▹ Unit) o; - -// Tail of a telescope. -symbol tl [n] : Sets (n +1) → Sets n; -rule tl (_ ▹ $ts) ↪ $ts; - - -// The definitions below do not depend on these rules; they only let the `Sets` -// argument stay implicit at use sites such as `congₙ 2 (+)`. -// So the unif rule below allows us to write generic programs acting on n-ary functions -// with less boilerplate. -// Unfolding `arrows` in the unifier. Its rules match on the `Sets` argument, -// so `arrows n ?ts ?b` is stuck when `?ts` is a metavariable: for -// `f : τ A → τ B → τ C` against `Arrow ?ts ?b`, the unifier faces -// `arrows 2 ?ts ?b ≡ A ⤳ B ⤳ C`. The rules below unfold it one step at a -// time, the constructor of `?ts`. -unif_rule @arrows ($n +1) $ts $b ≡ ($a ⤳ $c) ↪ [$ts ≡ @▹ $n $a _; @arrows $n (@tl $n $ts) $b ≡ $c]; -unif_rule @arrows 0 $ts $b ≡ $c ↪ [$ts ≡ Unit; $b ≡ $c]; +assert ⊢ Arrow (o ▹ o ▹ unit) o ≡ Prop → Prop → Prop; +assert ⊢ (∧) : Arrow (o ▹ o ▹ unit) o; // Helper type constructor to just create an arrow of `n`-times the type `t`. -// Ex: SetsIdent 3 nat ≡ nat ⤳ nat ⤳ nat -symbol SetsIdent n (t : Set) : Sets n; -rule SetsIdent 0 _ ↪ Unit -with SetsIdent ($n +1) $t ↪ $t ▹ (SetsIdent $n $t); +// Ex: sets_ident 3 nat ≡ nat ▹ nat ▹ nat ▹ unit +symbol sets_ident n (t : Set) : Sets n; +rule sets_ident 0 _ ↪ unit +with sets_ident ($n +1) $t ↪ $t ▹ sets_ident $n $t; -// Helper type constructor to just create an arrow of `n`-times the type `t`. -// Ex: ArrowI 2 nat ≡ nat ⤳ nat ⤳ nat -symbol ArrowI n (a : Set) ≔ Arrow (SetsIdent n a) a; // Arrow wrapper for SetsIdent +// Type of the `n`-ary functions on `a`. +// Ex: ArrowI 2 nat ≡ nat ⤳ nat ⤳ nat +symbol ArrowI n (a : Set) ≔ Arrow (sets_ident n a) a; -// ------------------------------------------------------ pointwise liftings -// Lift a unary operation (τ A → τ B) to n-ary functions. -symbol lift [A B : Set] n [dom : Sets n] : (τ A → τ B) → Arrow dom A → Arrow dom B; -rule @lift _ _ 0 Unit $op $f ↪ $op $f -with @lift $A $B ($n +1) ($t ▹ $ts) $op $f ↪ λ (x : τ $t), @lift $A $B $n $ts $op ($f x); +// Lift a unary operation (τ a → τ b) to n-ary functions. +symbol lift [a b : Set] n [dom : Sets n] : (τ a → τ b) → Arrow dom a → Arrow dom b; +rule @lift _ _ _ unit $op $f ↪ $op $f +with @lift _ _ _ ($t ▹ $ts) $op $f ↪ λ x : τ $t, @lift _ _ _ $ts $op ($f x); // Lift a binary operation to two n-ary functions with the same domain -symbol lift2 [A B C : Set] n [dom : Sets n] : - (τ A → τ B → τ C) → Arrow dom A → Arrow dom B → Arrow dom C; -rule @lift2 _ _ _ 0 Unit $op $f $g ↪ $op $f $g -with @lift2 $A $B $C ($n +1) ($t ▹ $ts) $op $f $g ↪ - λ (x : τ $t), @lift2 $A $B $C $n $ts $op ($f x) ($g x); +symbol lift2 [a b c : Set] n [dom : Sets n] : + (τ a → τ b → τ c) → Arrow dom a → Arrow dom b → Arrow dom c; +rule @lift2 _ _ _ _ unit $op $f $g ↪ $op $f $g +with @lift2 _ _ _ _ ($t ▹ $ts) $op $f $g ↪ λ x : τ $t, @lift2 _ _ _ _ $ts $op ($f x) ($g x); // `composeₙ n g f` precomposes the (n+1)-th argument of g with f: // composition with f, lifted over the first n arguments. symbol composeₙ [i j b : Set] n [dom : Sets n] (g : Arrow dom (j ⤳ b)) (f : τ i → τ j) : Arrow dom (i ⤳ b) ≔ lift n (λ h, h ∘ f) g; +symbol ∧ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 n (∧) p q; -symbol ∧ₙ [n] [dom : Sets n] (P Q : Arrow dom o) : Arrow dom o ≔ lift2 n (∧) P Q; +symbol ∨ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 n (∨) p q; -symbol ∨ₙ [n] [dom : Sets n] (P Q : Arrow dom o) : Arrow dom o ≔ lift2 n (∨) P Q; +symbol ⇒ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 n (⇒) p q; -symbol ⇒ₙ [n] [dom : Sets n] (P Q : Arrow dom o) : Arrow dom o ≔ lift2 n (⇒) P Q; +symbol quantₙ (q : Π a : Set, (τ a → Prop) → Prop) [n] [ts : Sets n] : Arrow ts o → Prop; +rule @quantₙ _ _ unit $p ↪ $p +with @quantₙ $q _ ($t ▹ $ts) $p ↪ $q $t (λ x : τ $t, @quantₙ $q _ $ts ($p x)); -symbol quantₙ (Q : Π a : Set, (τ a → Prop) → Prop) n [ts : Sets n] : Arrow ts o → Prop; -rule @quantₙ _ 0 Unit $P ↪ $P -with @quantₙ $Q ($n +1) ($t ▹ $ts) $P ↪ $Q $t (λ (x : τ $t), @quantₙ $Q $n $ts ($P x)); +symbol ∀ₙ n [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∀ p; +symbol ∃ₙ n [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∃ p; -symbol ∀ₙ n [ts : Sets n] (P : Arrow ts o) : Prop ≔ quantₙ (@∀) n P; -symbol ∃ₙ n [ts : Sets n] (P : Arrow ts o) : Prop ≔ quantₙ (@∃) n P; - -// Cong n f g computes the statement +// cong f g computes the statement // `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ f a₁ .. aₙ = g b₁ .. bₙ -symbol Cong n [ts : Sets n] [R : Set] (f g : Arrow ts R) : Prop; -rule @Cong 0 Unit $R $f $g ↪ @= $R $f $g -with @Cong ($n +1) ($t ▹ $ts) $R $f $g ↪ - `∀ (x : τ $t), `∀ (y : τ $t), (x = y) ⇒ @Cong $n $ts $R ($f x) ($g y); +symbol cong [n] [ts : Sets n] [r : Set] (f g : Arrow ts r) : Prop; +rule @cong _ unit _ $f $g ↪ $f = $g +with @cong _ ($t ▹ $ts) $r $f $g ↪ + `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ @cong _ $ts $r ($f x) ($g y); -opaque symbol congₙ [D : Set] n [ts : Sets n] (f : Arrow ts D) : π (@Cong n ts D f f) ≔ +opaque symbol congₙ [d : Set] n [ts : Sets n] (f : Arrow ts d) : π (cong f f) ≔ begin - assume D n; - refine ind_Sets (λ n u, `∀ f, @Cong n u D f f) _ _ n + assume d n; + refine ind_Sets (λ n u, `∀ f, @cong n u d f f) _ _ n { reflexivity } { assume m t ts ih; assume f t1 t2 hrefl; @@ -104,40 +84,54 @@ begin refine ih (f t2) } end; -// Subst n P Q computes the statement -// `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ P a₁ .. aₙ ⇒ Q b₁ .. bₙ -symbol Subst n [ts : Sets n] (P Q : Arrow ts o) : Prop; -rule @Subst 0 Unit $P $Q ↪ $P ⇒ $Q -with @Subst ($n +1) ($t ▹ $ts) $P $Q ↪ - `∀ (x : τ $t), `∀ (y : τ $t), (x = y) ⇒ @Subst $n $ts ($P x) ($Q y); +// subst p q computes the statement +// `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ p a₁ .. aₙ ⇒ q b₁ .. bₙ +symbol subst [n] [ts : Sets n] (p q : Arrow ts o) : Prop; +rule @subst _ unit $p $q ↪ $p ⇒ $q +with @subst _ ($t ▹ $ts) $p $q ↪ + `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ @subst _ $ts ($p x) ($q y); -opaque symbol substₙ n [ts : Sets n] (P : Arrow ts o) : π (@Subst n ts P P) ≔ +opaque symbol substₙ n [ts : Sets n] (p : Arrow ts o) : π (subst p p) ≔ begin assume n; - refine ind_Sets (λ n u, `∀ P, @Subst n u P P) _ _ n - { assume P h; refine h } + refine ind_Sets (λ n u, `∀ p, @subst n u p p) _ _ n + { assume p h; refine h } { assume m t ts ih; - assume P x y hxy; + assume p x y hxy; rewrite hxy; - refine ih (P y) } + refine ih (p y) } end; +symbol tl [n] : Sets (n +1) → Sets n; +rule tl (_ ▹ $ts) ↪ $ts; + +// The definitions above do not depend on the following unification rules: +// they only let the `Sets` argument stay implicit at use sites such as +// `congₙ 2 (+)`, where the arity `n` is given but the domain is not. +// The rules of `arrows` match on the `Sets` argument, so `arrows ?ts ?b` is +// stuck when `?ts` is a metavariable: for `f : τ a → τ b → τ c` against +// `Arrow ?ts ?d`, the unifier faces `arrows 2 ?ts ?d ≡ a ⤳ b ⤳ c`. The rules +// below unfold it one step at a time, guided by `n`, which determines the +// constructor of `?ts`. +unif_rule @arrows ($n +1) $ts $b ≡ ($a ⤳ $c) ↪ [$ts ≡ @▹ $n $a _; @arrows $n (@tl $n $ts) $b ≡ $c]; +unif_rule @arrows 0 $ts $b ≡ $c ↪ [$ts ≡ unit; $b ≡ $c]; + // Examples -private symbol f1 : Arrow (o ▹ o ▹ o ▹ o ▹ Unit) o; +private symbol f1 : Arrow (o ▹ o ▹ o ▹ o ▹ unit) o; private symbol f2 : ArrowI 4 o; private opaque symbol ex_cong a b c d x y w z : π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (f1 a b c d = f1 x y w z) ≔ begin assume a b c d x y w z heq1 heq2 heq3 heq4; -refine congₙ 4 f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 + refine congₙ 4 f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 end; assert (x y : ℕ) ⊢ let u1 ≔ composeₙ 1 (+) (λ x, x +1) in u1 x y ≡ x + (y +1); -private opaque symbol testSubst (P : Arrow (nat ▹ nat ▹ Unit) o) (a b x y : ℕ) : - π (a = x) → π (b = y) → π (P a b) → π (P x y) ≔ -begin assume P a b x y hax hby; refine substₙ 2 P _ _ hax _ _ hby end; \ No newline at end of file +private opaque symbol testSubst (p : Arrow (nat ▹ nat ▹ unit) o) (a b x y : ℕ) : + π (a = x) → π (b = y) → π (p a b) → π (p x y) ≔ +begin assume p a b x y hax hby; refine substₙ 2 p _ _ hax _ _ hby end; From a1c9903f5c68b8024d5109cbb75da4a016ff19bf Mon Sep 17 00:00:00 2001 From: NotBad4U Date: Fri, 18 Sep 2026 10:49:08 +0200 Subject: [PATCH 3/6] Add injective on type Arrow, set_idents, sets, ArrowI; remove @; make arity of the function implicit --- NaryFunctions.lp | 129 +++++++++++++++++++++++++++++------------------ 1 file changed, 79 insertions(+), 50 deletions(-) diff --git a/NaryFunctions.lp b/NaryFunctions.lp index 8e6f6ca..651fa9e 100644 --- a/NaryFunctions.lp +++ b/NaryFunctions.lp @@ -13,11 +13,14 @@ inductive Sets : ℕ → TYPE ≔ notation ▹ infix right 10; -symbol sets (n : ℕ) : Set; +constant symbol sets (n : ℕ) : Set; rule τ (sets $n) ↪ Sets $n; +symbol tl [n] : Sets (n +1) → Sets n; +rule tl (_ ▹ $ts) ↪ $ts; + // Type transformer x1 ▹ x2 ▹ .. into x1 ⤳ x2 ⤳ .. -symbol arrows [n] : Sets n → Set → Set; +injective symbol arrows [n] : Sets n → Set → Set; rule arrows unit $b ↪ $b with arrows ($t ▹ $ts) $b ↪ $t ⤳ arrows $ts $b; @@ -28,55 +31,62 @@ assert ⊢ (∧) : Arrow (o ▹ o ▹ unit) o; // Helper type constructor to just create an arrow of `n`-times the type `t`. // Ex: sets_ident 3 nat ≡ nat ▹ nat ▹ nat ▹ unit -symbol sets_ident n (t : Set) : Sets n; +injective symbol sets_ident n (t : Set) : Sets n; rule sets_ident 0 _ ↪ unit with sets_ident ($n +1) $t ↪ $t ▹ sets_ident $n $t; // Type of the `n`-ary functions on `a`. // Ex: ArrowI 2 nat ≡ nat ⤳ nat ⤳ nat -symbol ArrowI n (a : Set) ≔ Arrow (sets_ident n a) a; +injective symbol ArrowI n (a : Set) ≔ Arrow (sets_ident n a) a; // Lift a unary operation (τ a → τ b) to n-ary functions. -symbol lift [a b : Set] n [dom : Sets n] : (τ a → τ b) → Arrow dom a → Arrow dom b; -rule @lift _ _ _ unit $op $f ↪ $op $f -with @lift _ _ _ ($t ▹ $ts) $op $f ↪ λ x : τ $t, @lift _ _ _ $ts $op ($f x); +symbol lift [a b : Set] [n] (dom : Sets n) : (τ a → τ b) → Arrow dom a → Arrow dom b; +rule lift unit $op $f ↪ $op $f +with lift ($t ▹ $ts) $op $f ↪ λ x : τ $t, lift $ts $op ($f x); // Lift a binary operation to two n-ary functions with the same domain -symbol lift2 [a b c : Set] n [dom : Sets n] : +symbol lift2 [a b c : Set] [n] (dom : Sets n) : (τ a → τ b → τ c) → Arrow dom a → Arrow dom b → Arrow dom c; -rule @lift2 _ _ _ _ unit $op $f $g ↪ $op $f $g -with @lift2 _ _ _ _ ($t ▹ $ts) $op $f $g ↪ λ x : τ $t, @lift2 _ _ _ _ $ts $op ($f x) ($g x); +rule lift2 unit $op $f $g ↪ $op $f $g +with lift2 ($t ▹ $ts) $op $f $g ↪ λ x : τ $t, lift2 $ts $op ($f x) ($g x); -// `composeₙ n g f` precomposes the (n+1)-th argument of g with f: -// composition with f, lifted over the first n arguments. -symbol composeₙ [i j b : Set] n [dom : Sets n] (g : Arrow dom (j ⤳ b)) (f : τ i → τ j) - : Arrow dom (i ⤳ b) ≔ lift n (λ h, h ∘ f) g; +// `composeₙ dom g f` precomposes the argument after `dom` with `f`: +// composition with `f`, lifted over the arguments listed in `dom`. +// It takes the domain rather than the arity because it wants a *partial* +// decomposition of the type of `g` — `Arrow dom (j ⤳ b)`, not all the way down +// — and the rules below decompose maximally. With `dom` given there is nothing +// left to guess. +symbol composeₙ [i j b : Set] [n] (dom : Sets n) (g : Arrow dom (j ⤳ b)) (f : τ i → τ j) + : Arrow dom (i ⤳ b) ≔ lift dom (λ h, h ∘ f) g; -symbol ∧ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 n (∧) p q; +symbol ∧ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 dom (∧) p q; -symbol ∨ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 n (∨) p q; +symbol ∨ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 dom (∨) p q; -symbol ⇒ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 n (⇒) p q; +symbol ⇒ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 dom (⇒) p q; -symbol quantₙ (q : Π a : Set, (τ a → Prop) → Prop) [n] [ts : Sets n] : Arrow ts o → Prop; -rule @quantₙ _ _ unit $p ↪ $p -with @quantₙ $q _ ($t ▹ $ts) $p ↪ $q $t (λ x : τ $t, @quantₙ $q _ $ts ($p x)); +symbol quantₙ (q : Π a : Set, (τ a → Prop) → Prop) [n] (ts : Sets n) : Arrow ts o → Prop; +rule quantₙ _ unit $p ↪ $p +with quantₙ $q ($t ▹ $ts) $p ↪ $q $t (λ x : τ $t, quantₙ $q $ts ($p x)); -symbol ∀ₙ n [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∀ p; -symbol ∃ₙ n [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∃ p; +symbol ∀ₙ [n] [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∀ ts p; +symbol ∃ₙ [n] [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∃ ts p; // cong f g computes the statement // `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ f a₁ .. aₙ = g b₁ .. bₙ -symbol cong [n] [ts : Sets n] [r : Set] (f g : Arrow ts r) : Prop; -rule @cong _ unit _ $f $g ↪ $f = $g -with @cong _ ($t ▹ $ts) $r $f $g ↪ - `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ @cong _ $ts $r ($f x) ($g y); - -opaque symbol congₙ [d : Set] n [ts : Sets n] (f : Arrow ts d) : π (cong f f) ≔ +symbol cong [n] (ts : Sets n) [r : Set] (f g : Arrow ts r) : Prop; +rule cong unit $f $g ↪ $f = $g +with cong ($t ▹ $ts) $f $g ↪ + `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ cong $ts ($f x) ($g y); + +// `congₙ f` never takes an arity: `ts` determines `n`, and `ts` is recovered +// from the type of `f` — directly when that type is headed by `arrows`, and +// otherwise by the unification rules below, which peel it off the arrows. +opaque symbol congₙ [d : Set] [n] [ts : Sets n] (f : Arrow ts d) : π (cong ts f f) ≔ begin assume d n; - refine ind_Sets (λ n u, `∀ f, @cong n u d f f) _ _ n + refine ind_Sets (λ n u, `∀ f, cong u f f) _ _ n { reflexivity } { assume m t ts ih; assume f t1 t2 hrefl; @@ -84,17 +94,18 @@ begin refine ih (f t2) } end; + // subst p q computes the statement // `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ p a₁ .. aₙ ⇒ q b₁ .. bₙ -symbol subst [n] [ts : Sets n] (p q : Arrow ts o) : Prop; -rule @subst _ unit $p $q ↪ $p ⇒ $q -with @subst _ ($t ▹ $ts) $p $q ↪ - `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ @subst _ $ts ($p x) ($q y); +symbol subst [n] (ts : Sets n) (p q : Arrow ts o) : Prop; +rule subst unit $p $q ↪ $p ⇒ $q +with subst ($t ▹ $ts) $p $q ↪ + `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ subst $ts ($p x) ($q y); -opaque symbol substₙ n [ts : Sets n] (p : Arrow ts o) : π (subst p p) ≔ +opaque symbol substₙ [n] [ts : Sets n] (p : Arrow ts o) : π (subst ts p p) ≔ begin assume n; - refine ind_Sets (λ n u, `∀ p, @subst n u p p) _ _ n + refine ind_Sets (λ n u, `∀ p, subst u p p) _ _ n { assume p h; refine h } { assume m t ts ih; assume p x y hxy; @@ -102,8 +113,16 @@ begin refine ih (p y) } end; -symbol tl [n] : Sets (n +1) → Sets n; -rule tl (_ ▹ $ts) ↪ $ts; +// Examples + +private symbol f1 : Arrow (o ▹ o ▹ o ▹ o ▹ unit) o; + +private opaque symbol ex_cong a b c d x y w z : + π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (f1 a b c d = f1 x y w z) ≔ +begin + assume a b c d x y w z heq1 heq2 heq3 heq4; + refine congₙ f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 +end; // The definitions above do not depend on the following unification rules: // they only let the `Sets` argument stay implicit at use sites such as @@ -113,25 +132,35 @@ rule tl (_ ▹ $ts) ↪ $ts; // `Arrow ?ts ?d`, the unifier faces `arrows 2 ?ts ?d ≡ a ⤳ b ⤳ c`. The rules // below unfold it one step at a time, guided by `n`, which determines the // constructor of `?ts`. -unif_rule @arrows ($n +1) $ts $b ≡ ($a ⤳ $c) ↪ [$ts ≡ @▹ $n $a _; @arrows $n (@tl $n $ts) $b ≡ $c]; -unif_rule @arrows 0 $ts $b ≡ $c ↪ [$ts ≡ unit; $b ≡ $c]; - -// Examples - -private symbol f1 : Arrow (o ▹ o ▹ o ▹ o ▹ unit) o; -private symbol f2 : ArrowI 4 o; +unif_rule arrows $ts $b ≡ ($a ⤳ $c) ↪ [$ts ≡ @▹ _ $a _; @arrows _ (@tl _ $ts) $b ≡ $c]; +unif_rule arrows $ts $b ≡ $c ↪ [$ts ≡ unit; $b ≡ $c]; + +// The same function f1 as a *parameter* loses the head entirely: a binder's type +// is normalised, so `Arrow (o ▹ o ▹ o ▹ o ▹ unit) o` becomes +// `Π _ _ _ _, τ (arrows unit o)`. The unif_rule allows to compare the two forms. +private opaque symbol ex_cong_param a b c d x y w z + (g : Arrow (o ▹ o ▹ o ▹ o ▹ unit) o) : + π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (g a b c d = g x y w z) ≔ +begin + assume a b c d x y w z g heq1 heq2 heq3 heq4; + refine congₙ g _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 +end; -private opaque symbol ex_cong a b c d x y w z : - π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (f1 a b c d = f1 x y w z) ≔ +// A function declared with an ordinary arrow type such as `+ : ℕ → ℕ → ℕ` +// mentions no `Sets` at all, and `congₙ (+)` leaves the stuck +// constraint `arrows ?ts ?d ≡ ℕ → ℕ → ℕ` for the rules to unfold. +// So the unif_rule unfold this constraints and allows to solve the constraints. +private opaque symbol ex_cong_add (a b x y : ℕ) : + π (a = x) → π (b = y) → π (a + b = x + y) ≔ begin - assume a b c d x y w z heq1 heq2 heq3 heq4; - refine congₙ 4 f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 + assume a b x y h1 h2; + refine congₙ (+) _ _ h1 _ _ h2 end; assert (x y : ℕ) - ⊢ let u1 ≔ composeₙ 1 (+) (λ x, x +1) in + ⊢ let u1 ≔ composeₙ (nat ▹ unit) (+) (λ x, x +1) in u1 x y ≡ x + (y +1); private opaque symbol testSubst (p : Arrow (nat ▹ nat ▹ unit) o) (a b x y : ℕ) : π (a = x) → π (b = y) → π (p a b) → π (p x y) ≔ -begin assume p a b x y hax hby; refine substₙ 2 p _ _ hax _ _ hby end; +begin assume p a b x y hax hby; refine substₙ p _ _ hax _ _ hby end; From 1d0647a31fffcd2e8b644434c29197b5f325175a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 23 Sep 2026 18:27:57 +0200 Subject: [PATCH 4/6] remove unsound unification rules + rename some symbols --- HOL.lp | 2 +- NaryFunctions.lp | 215 +++++++++++++++++++++-------------------------- 2 files changed, 99 insertions(+), 118 deletions(-) diff --git a/HOL.lp b/HOL.lp index 662baa6..08dd3bf 100644 --- a/HOL.lp +++ b/HOL.lp @@ -14,7 +14,7 @@ rule $a ⤳d λ _,$b.[] ↪ $a ⤳ $b; rule τ ($a ⤳d λ x,$b.[x]) ↪ Π x:τ $a, τ $b.[x]; -// function composition +// function composition \circ symbol ∘ [a b c] : τ (b ⤳ c) → τ (a ⤳ b) → τ a → τ c ≔ λ g f x, g (f x); notation ∘ infix 20; diff --git a/NaryFunctions.lp b/NaryFunctions.lp index 651fa9e..5a47fc6 100644 --- a/NaryFunctions.lp +++ b/NaryFunctions.lp @@ -1,166 +1,147 @@ -// Implementation of N-ary functions and relations based on Guillaume Allais, -// "Generic Level Polymorphic N-ary Functions" (TyDe 2019). -// This API provides n-ary functions which automatically reconstruct the representation of their inputs' types by unification. -// It helps to define fully level polymorphic n-ary versions of congruence, substitution and the combinators for indexed families, -// that are used by programs such as SMT solvers. Lemmas provided in the rest of the library such as `Eq.lp` are implemented for -// fixed arities, and the implementation here aims to provide similar lemmas for N-ary Combinators. +/* N-ary functions and relations -require open Stdlib.Set Stdlib.Prop Stdlib.FOL Stdlib.HOL Stdlib.Nat Stdlib.Eq Stdlib.Impred; +following "Generic Level Polymorphic N-ary Functions" by Guillaume +Allais (TyDe 2019). -inductive Sets : ℕ → TYPE ≔ -| unit : Sets 0 -| ▹ : Π [n : ℕ], Set → Sets n → Sets (n +1); +This API provides n-ary functions which automatically reconstruct the +representation of their inputs' types by unification. It helps to +define fully level polymorphic n-ary versions of congruence, +substitution and the combinators for indexed families, that are used +by programs such as SMT solvers. Lemmas provided in the rest of the +library such as `Eq.lp` are implemented for fixed arities, and the +implementation here aims to provide similar lemmas for N-ary +combinators. */ -notation ▹ infix right 10; +require open Stdlib.HOL Stdlib.Nat; -constant symbol sets (n : ℕ) : Set; -rule τ (sets $n) ↪ Sets $n; + // vectors of type codes +inductive VSet : ℕ → TYPE ≔ + | unit : VSet 0 + | ▹ : Set → Π [n], VSet n → VSet (n +1); // \smalltriangleright -symbol tl [n] : Sets (n +1) → Sets n; -rule tl (_ ▹ $ts) ↪ $ts; +notation ▹ infix right 10; -// Type transformer x1 ▹ x2 ▹ .. into x1 ⤳ x2 ⤳ .. -injective symbol arrows [n] : Sets n → Set → Set; -rule arrows unit $b ↪ $b -with arrows ($t ▹ $ts) $b ↪ $t ⤳ arrows $ts $b; +// tail +symbol tl [n] : VSet (n +1) → VSet n; +rule tl (_ ▹ $ts) ↪ $ts; -injective symbol Arrow [n] (dom : Sets n) (cod : Set) : TYPE ≔ τ (arrows dom cod); +// constant vector +injective symbol vcst n (t : Set) : VSet n; +rule vcst 0 _ ↪ unit +with vcst ($n +1) $t ↪ $t ▹ vcst $n $t; -assert ⊢ Arrow (o ▹ o ▹ unit) o ≡ Prop → Prop → Prop; -assert ⊢ (∧) : Arrow (o ▹ o ▹ unit) o; +// type code of n-ary functions: fun (a₁ ▹ … ▹ aₙ ▹ unit) b ≡ a₁ ⤳ … ⤳ aₙ ⤳ b +symbol fun [n] : VSet n → Set → Set; +rule fun unit $b ↪ $b +with fun ($t ▹ $ts) $b ↪ $t ⤳ fun $ts $b; -// Helper type constructor to just create an arrow of `n`-times the type `t`. -// Ex: sets_ident 3 nat ≡ nat ▹ nat ▹ nat ▹ unit -injective symbol sets_ident n (t : Set) : Sets n; -rule sets_ident 0 _ ↪ unit -with sets_ident ($n +1) $t ↪ $t ▹ sets_ident $n $t; +// fun is not injective, however (fun d) and (fun _ b) are both injective +// we can therefore safely add the following unification rules: +unif_rule fun $x $y ≡ fun $x $y' ↪ [$y ≡ $y']; +unif_rule fun $x $y ≡ fun $x' $y ↪ [$x ≡ $x']; +unif_rule fun $x $y ≡ $y ↪ [$x ≡ unit]; -// Type of the `n`-ary functions on `a`. -// Ex: ArrowI 2 nat ≡ nat ⤳ nat ⤳ nat -injective symbol ArrowI n (a : Set) ≔ Arrow (sets_ident n a) a; +// type of n-ary functions: Fun +symbol Fun [n] (dom : VSet n) cod ≔ τ (fun dom cod); +// type of n-ary endofunctions +injective symbol Endo n a ≔ Fun (vcst n a) a; -// Lift a unary operation (τ a → τ b) to n-ary functions. -symbol lift [a b : Set] [n] (dom : Sets n) : (τ a → τ b) → Arrow dom a → Arrow dom b; +// lift (a₁ ▹ … ▹ aₙ ▹ unit) p f x₁ … xₙ ≡ p (f x₁ … xₙ) +symbol lift [a b n] (d: VSet n): (τ a → τ b) → Fun d a → Fun d b; rule lift unit $op $f ↪ $op $f -with lift ($t ▹ $ts) $op $f ↪ λ x : τ $t, lift $ts $op ($f x); - -// Lift a binary operation to two n-ary functions with the same domain -symbol lift2 [a b c : Set] [n] (dom : Sets n) : - (τ a → τ b → τ c) → Arrow dom a → Arrow dom b → Arrow dom c; -rule lift2 unit $op $f $g ↪ $op $f $g -with lift2 ($t ▹ $ts) $op $f $g ↪ λ x : τ $t, lift2 $ts $op ($f x) ($g x); +with lift (_ ▹ $ts) $op $f ↪ λ x, lift $ts $op ($f x); -// `composeₙ dom g f` precomposes the argument after `dom` with `f`: -// composition with `f`, lifted over the arguments listed in `dom`. -// It takes the domain rather than the arity because it wants a *partial* -// decomposition of the type of `g` — `Arrow dom (j ⤳ b)`, not all the way down -// — and the rules below decompose maximally. With `dom` given there is nothing -// left to guess. -symbol composeₙ [i j b : Set] [n] (dom : Sets n) (g : Arrow dom (j ⤳ b)) (f : τ i → τ j) - : Arrow dom (i ⤳ b) ≔ lift dom (λ h, h ∘ f) g; - -symbol ∧ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 dom (∧) p q; - -symbol ∨ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 dom (∨) p q; - -symbol ⇒ₙ [n] [dom : Sets n] (p q : Arrow dom o) : Arrow dom o ≔ lift2 dom (⇒) p q; - -symbol quantₙ (q : Π a : Set, (τ a → Prop) → Prop) [n] (ts : Sets n) : Arrow ts o → Prop; -rule quantₙ _ unit $p ↪ $p -with quantₙ $q ($t ▹ $ts) $p ↪ $q $t (λ x : τ $t, quantₙ $q $ts ($p x)); +// comp (a₁ ▹ … ▹ aₙ ▹ unit) g f x₁ … xₙ ≡ g x₁ … xₙ ∘ f +symbol comp [n] (d: VSet n) [j b] (g: Fun d (j ⤳ b)) [i] (f: τ i → τ j) + : Fun d (i ⤳ b) ≔ lift d (λ h:_ → τ b, h ∘ f) g; -symbol ∀ₙ [n] [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∀ ts p; -symbol ∃ₙ [n] [ts : Sets n] (p : Arrow ts o) : Prop ≔ quantₙ @∃ ts p; +// lift2 (a₁ ▹ … ▹ aₙ ▹ unit) p f g x₁ … xₙ ≡ p (f x₁ … xₙ) (g x₁ … xₙ) +symbol lift2 [a b c n] (d: VSet n) : + (τ a → τ b → τ c) → Fun d a → Fun d b → Fun d c; +rule lift2 unit $op $f $g ↪ $op $f $g +with lift2 (_ ▹ $ts) $op $f $g ↪ λ x, lift2 $ts $op ($f x) ($g x); -// cong f g computes the statement -// `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ f a₁ .. aₙ = g b₁ .. bₙ -symbol cong [n] (ts : Sets n) [r : Set] (f g : Arrow ts r) : Prop; +// cong (a₁ ▹ … ▹ aₙ ▹ unit) r f g ≡ +// `∀ x₁,`∀ y₁, x₁ = y₁ ⇒ … ⇒ `∀ xₙ,`∀ yₙ, xₙ = yₙ ⇒ f x₁ … xₙ = g y₁ … yₙ +// we can declare r as implicit thanks to the unif_rule on Fun +symbol cong [n] (ts: VSet n) [r] (f g: Fun ts r): Prop; rule cong unit $f $g ↪ $f = $g -with cong ($t ▹ $ts) $f $g ↪ - `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ cong $ts ($f x) ($g y); +with cong (_ ▹ $ts) $f $g ↪ `∀ x,`∀ y, x = y ⇒ cong $ts ($f x) ($g y); -// `congₙ f` never takes an arity: `ts` determines `n`, and `ts` is recovered -// from the type of `f` — directly when that type is headed by `arrows`, and -// otherwise by the unification rules below, which peel it off the arrows. -opaque symbol congₙ [d : Set] [n] [ts : Sets n] (f : Arrow ts d) : π (cong ts f f) ≔ +// we can declare r as implicit thanks to the unif_rule on Fun +opaque symbol refl_cong [n] (ts: VSet n) [r] (f: Fun ts r): π(cong ts f f) ≔ begin - assume d n; - refine ind_Sets (λ n u, `∀ f, cong u f f) _ _ n - { reflexivity } - { assume m t ts ih; - assume f t1 t2 hrefl; - rewrite hrefl; - refine ih (f t2) } + have aux: Π r n (ts: VSet n) (f: Fun ts r), π(cong ts f f) { + assume r n; refine ind_VSet (λ n ts, `∀ f, cong ts [r] f f) _ _ n + { reflexivity } + { assume t m ts ih f x y xy; rewrite xy; refine ih (f y) } + }; + assume n ts r; refine aux r n ts end; +require open Stdlib.Impred; -// subst p q computes the statement -// `∀ a₁, `∀ b₁, a₁ = b₁ ⇒ ... ⇒ `∀ aₙ, `∀ bₙ, aₙ = bₙ ⇒ p a₁ .. aₙ ⇒ q b₁ .. bₙ -symbol subst [n] (ts : Sets n) (p q : Arrow ts o) : Prop; -rule subst unit $p $q ↪ $p ⇒ $q -with subst ($t ▹ $ts) $p $q ↪ - `∀ x : τ $t, `∀ y : τ $t, x = y ⇒ subst $ts ($p x) ($q y); +// subst (a₁ ▹ … ▹ aₙ ▹ unit) f g ≡ +// `∀x₁:τa₁,`∀y₁, x₁ = y₁ ⇒ … ⇒ `∀xₙ:τaₙ,`∀yₙ, xₙ = yₙ ⇒ f x₁ … xₙ ⇒ g y₁ … yₙ +symbol subst [n] (ts: VSet n) (f g: Fun ts o): Prop; +rule subst unit $f $g ↪ $f ⇒ $g +with subst (_ ▹ $ts) $f $g ↪ `∀ x,`∀ y, x = y ⇒ subst $ts ($f x) ($g y); -opaque symbol substₙ [n] [ts : Sets n] (p : Arrow ts o) : π (subst ts p p) ≔ +opaque symbol refl_subst [n] (ts: VSet n) (p: Fun ts o): π(subst ts p p) ≔ begin - assume n; - refine ind_Sets (λ n u, `∀ p, subst u p p) _ _ n + assume n; refine ind_VSet (λ n ts, `∀ p, subst ts p p) _ _ n { assume p h; refine h } - { assume m t ts ih; - assume p x y hxy; - rewrite hxy; - refine ih (p y) } + { assume t m ts ih p x y xy; rewrite xy; refine ih (p y) } end; -// Examples +// Lifted connectors + +symbol ∧ₙ [n] [d: VSet n] ≔ lift2 d (∧); + +symbol ∨ₙ [n] [d: VSet n] ≔ lift2 d (∨); + +symbol ⇒ₙ [n] [d: VSet n] ≔ lift2 d (⇒); + +// quantₙ Q (a₁ ▹ … ▹ aₙ ▹ unit) p ≡ `Q x₁, …, `Q xₙ, p x₁ … xₙ +symbol quantₙ (q: Π a, (τ a → Prop) → Prop) [n] (ts: VSet n): Fun ts o → Prop; +rule quantₙ _ unit $p ↪ $p +with quantₙ $q ($t ▹ $ts) $p ↪ $q $t (λ x, quantₙ $q $ts ($p x)); + +symbol ∀ₙ [n] ≔ @quantₙ @∀ n; +symbol ∃ₙ [n] ≔ @quantₙ @∃ n; + +// Tests -private symbol f1 : Arrow (o ▹ o ▹ o ▹ o ▹ unit) o; +private symbol f1 : Endo 4 o; private opaque symbol ex_cong a b c d x y w z : π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (f1 a b c d = f1 x y w z) ≔ begin assume a b c d x y w z heq1 heq2 heq3 heq4; - refine congₙ f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 + refine refl_cong (o ▹ o ▹ o ▹ o ▹ unit) f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 end; -// The definitions above do not depend on the following unification rules: -// they only let the `Sets` argument stay implicit at use sites such as -// `congₙ 2 (+)`, where the arity `n` is given but the domain is not. -// The rules of `arrows` match on the `Sets` argument, so `arrows ?ts ?b` is -// stuck when `?ts` is a metavariable: for `f : τ a → τ b → τ c` against -// `Arrow ?ts ?d`, the unifier faces `arrows 2 ?ts ?d ≡ a ⤳ b ⤳ c`. The rules -// below unfold it one step at a time, guided by `n`, which determines the -// constructor of `?ts`. -unif_rule arrows $ts $b ≡ ($a ⤳ $c) ↪ [$ts ≡ @▹ _ $a _; @arrows _ (@tl _ $ts) $b ≡ $c]; -unif_rule arrows $ts $b ≡ $c ↪ [$ts ≡ unit; $b ≡ $c]; - -// The same function f1 as a *parameter* loses the head entirely: a binder's type -// is normalised, so `Arrow (o ▹ o ▹ o ▹ o ▹ unit) o` becomes -// `Π _ _ _ _, τ (arrows unit o)`. The unif_rule allows to compare the two forms. private opaque symbol ex_cong_param a b c d x y w z - (g : Arrow (o ▹ o ▹ o ▹ o ▹ unit) o) : + (g : Fun (o ▹ o ▹ o ▹ o ▹ unit) o) : π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (g a b c d = g x y w z) ≔ begin assume a b c d x y w z g heq1 heq2 heq3 heq4; - refine congₙ g _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 + refine refl_cong (o ▹ o ▹ o ▹ o ▹ unit) g _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 end; -// A function declared with an ordinary arrow type such as `+ : ℕ → ℕ → ℕ` -// mentions no `Sets` at all, and `congₙ (+)` leaves the stuck -// constraint `arrows ?ts ?d ≡ ℕ → ℕ → ℕ` for the rules to unfold. -// So the unif_rule unfold this constraints and allows to solve the constraints. private opaque symbol ex_cong_add (a b x y : ℕ) : π (a = x) → π (b = y) → π (a + b = x + y) ≔ begin assume a b x y h1 h2; - refine congₙ (+) _ _ h1 _ _ h2 + refine refl_cong (nat ▹ nat ▹ unit) (+) _ _ h1 _ _ h2 end; -assert (x y : ℕ) - ⊢ let u1 ≔ composeₙ (nat ▹ unit) (+) (λ x, x +1) in - u1 x y ≡ x + (y +1); +assert x y ⊢ let u ≔ comp (nat ▹ unit) (+) (+1) in u x y ≡ x + (y +1); -private opaque symbol testSubst (p : Arrow (nat ▹ nat ▹ unit) o) (a b x y : ℕ) : +private opaque symbol testSubst (p: Fun (nat ▹ nat ▹ unit) o) a b x y: π (a = x) → π (b = y) → π (p a b) → π (p x y) ≔ -begin assume p a b x y hax hby; refine substₙ p _ _ hax _ _ hby end; +begin + assume p a b x y ax by; + refine refl_subst (nat ▹ nat ▹ unit) p _ _ ax _ _ by +end; From 4bdc805c1a3e36d833d12a28dcc2f822ee2c8716 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 25 Sep 2026 07:38:34 +0200 Subject: [PATCH 5/6] details --- NaryFunctions.lp => NaryFun.lp | 74 ++++++++++++++-------------------- 1 file changed, 30 insertions(+), 44 deletions(-) rename NaryFunctions.lp => NaryFun.lp (62%) diff --git a/NaryFunctions.lp b/NaryFun.lp similarity index 62% rename from NaryFunctions.lp rename to NaryFun.lp index 5a47fc6..69c7522 100644 --- a/NaryFunctions.lp +++ b/NaryFun.lp @@ -1,23 +1,14 @@ -/* N-ary functions and relations +/* n-ary functions and relations following "Generic Level Polymorphic N-ary Functions" by Guillaume -Allais (TyDe 2019). - -This API provides n-ary functions which automatically reconstruct the -representation of their inputs' types by unification. It helps to -define fully level polymorphic n-ary versions of congruence, -substitution and the combinators for indexed families, that are used -by programs such as SMT solvers. Lemmas provided in the rest of the -library such as `Eq.lp` are implemented for fixed arities, and the -implementation here aims to provide similar lemmas for N-ary -combinators. */ +Allais (TyDe 2019). */ require open Stdlib.HOL Stdlib.Nat; - // vectors of type codes +// vectors of type codes inductive VSet : ℕ → TYPE ≔ - | unit : VSet 0 - | ▹ : Set → Π [n], VSet n → VSet (n +1); // \smalltriangleright +| ◃ : VSet 0 // \smalltriangleleft +| ▹ : Set → Π [n], VSet n → VSet (n +1); // \smalltriangleright notation ▹ infix right 10; @@ -27,49 +18,47 @@ rule tl (_ ▹ $ts) ↪ $ts; // constant vector injective symbol vcst n (t : Set) : VSet n; -rule vcst 0 _ ↪ unit +rule vcst 0 _ ↪ ◃ with vcst ($n +1) $t ↪ $t ▹ vcst $n $t; -// type code of n-ary functions: fun (a₁ ▹ … ▹ aₙ ▹ unit) b ≡ a₁ ⤳ … ⤳ aₙ ⤳ b +// type code of n-ary functions: fun (a₁ ▹ … ▹ aₙ ▹ ◃) b ≡ a₁ ⤳ … ⤳ aₙ ⤳ b symbol fun [n] : VSet n → Set → Set; -rule fun unit $b ↪ $b +rule fun ◃ $b ↪ $b with fun ($t ▹ $ts) $b ↪ $t ⤳ fun $ts $b; // fun is not injective, however (fun d) and (fun _ b) are both injective // we can therefore safely add the following unification rules: unif_rule fun $x $y ≡ fun $x $y' ↪ [$y ≡ $y']; unif_rule fun $x $y ≡ fun $x' $y ↪ [$x ≡ $x']; -unif_rule fun $x $y ≡ $y ↪ [$x ≡ unit]; +unif_rule fun $x $y ≡ $y ↪ [$x ≡ ◃]; -// type of n-ary functions: Fun +// type of n-ary functions symbol Fun [n] (dom : VSet n) cod ≔ τ (fun dom cod); // type of n-ary endofunctions injective symbol Endo n a ≔ Fun (vcst n a) a; -// lift (a₁ ▹ … ▹ aₙ ▹ unit) p f x₁ … xₙ ≡ p (f x₁ … xₙ) +// lift (a₁ ▹ … ▹ aₙ ▹ ◃) p f x₁ … xₙ ≡ p (f x₁ … xₙ) symbol lift [a b n] (d: VSet n): (τ a → τ b) → Fun d a → Fun d b; -rule lift unit $op $f ↪ $op $f +rule lift ◃ $op $f ↪ $op $f with lift (_ ▹ $ts) $op $f ↪ λ x, lift $ts $op ($f x); -// comp (a₁ ▹ … ▹ aₙ ▹ unit) g f x₁ … xₙ ≡ g x₁ … xₙ ∘ f +// comp (a₁ ▹ … ▹ aₙ ▹ ◃) g f x₁ … xₙ ≡ g x₁ … xₙ ∘ f symbol comp [n] (d: VSet n) [j b] (g: Fun d (j ⤳ b)) [i] (f: τ i → τ j) : Fun d (i ⤳ b) ≔ lift d (λ h:_ → τ b, h ∘ f) g; -// lift2 (a₁ ▹ … ▹ aₙ ▹ unit) p f g x₁ … xₙ ≡ p (f x₁ … xₙ) (g x₁ … xₙ) +// lift2 (a₁ ▹ … ▹ aₙ ▹ ◃) p f g x₁ … xₙ ≡ p (f x₁ … xₙ) (g x₁ … xₙ) symbol lift2 [a b c n] (d: VSet n) : (τ a → τ b → τ c) → Fun d a → Fun d b → Fun d c; -rule lift2 unit $op $f $g ↪ $op $f $g +rule lift2 ◃ $op $f $g ↪ $op $f $g with lift2 (_ ▹ $ts) $op $f $g ↪ λ x, lift2 $ts $op ($f x) ($g x); -// cong (a₁ ▹ … ▹ aₙ ▹ unit) r f g ≡ +// cong (a₁ ▹ … ▹ aₙ ▹ ◃) r f g ≡ // `∀ x₁,`∀ y₁, x₁ = y₁ ⇒ … ⇒ `∀ xₙ,`∀ yₙ, xₙ = yₙ ⇒ f x₁ … xₙ = g y₁ … yₙ -// we can declare r as implicit thanks to the unif_rule on Fun symbol cong [n] (ts: VSet n) [r] (f g: Fun ts r): Prop; -rule cong unit $f $g ↪ $f = $g +rule cong ◃ $f $g ↪ $f = $g with cong (_ ▹ $ts) $f $g ↪ `∀ x,`∀ y, x = y ⇒ cong $ts ($f x) ($g y); -// we can declare r as implicit thanks to the unif_rule on Fun opaque symbol refl_cong [n] (ts: VSet n) [r] (f: Fun ts r): π(cong ts f f) ≔ begin have aux: Π r n (ts: VSet n) (f: Fun ts r), π(cong ts f f) { @@ -82,10 +71,10 @@ end; require open Stdlib.Impred; -// subst (a₁ ▹ … ▹ aₙ ▹ unit) f g ≡ +// subst (a₁ ▹ … ▹ aₙ ▹ ◃) f g ≡ // `∀x₁:τa₁,`∀y₁, x₁ = y₁ ⇒ … ⇒ `∀xₙ:τaₙ,`∀yₙ, xₙ = yₙ ⇒ f x₁ … xₙ ⇒ g y₁ … yₙ symbol subst [n] (ts: VSet n) (f g: Fun ts o): Prop; -rule subst unit $f $g ↪ $f ⇒ $g +rule subst ◃ $f $g ↪ $f ⇒ $g with subst (_ ▹ $ts) $f $g ↪ `∀ x,`∀ y, x = y ⇒ subst $ts ($f x) ($g y); opaque symbol refl_subst [n] (ts: VSet n) (p: Fun ts o): π(subst ts p p) ≔ @@ -95,23 +84,20 @@ begin { assume t m ts ih p x y xy; rewrite xy; refine ih (p y) } end; -// Lifted connectors - +// lifted connectors symbol ∧ₙ [n] [d: VSet n] ≔ lift2 d (∧); - symbol ∨ₙ [n] [d: VSet n] ≔ lift2 d (∨); - symbol ⇒ₙ [n] [d: VSet n] ≔ lift2 d (⇒); -// quantₙ Q (a₁ ▹ … ▹ aₙ ▹ unit) p ≡ `Q x₁, …, `Q xₙ, p x₁ … xₙ +// quantₙ Q (a₁ ▹ … ▹ aₙ ▹ ◃) p ≡ `Q x₁, …, `Q xₙ, p x₁ … xₙ symbol quantₙ (q: Π a, (τ a → Prop) → Prop) [n] (ts: VSet n): Fun ts o → Prop; -rule quantₙ _ unit $p ↪ $p +rule quantₙ _ ◃ $p ↪ $p with quantₙ $q ($t ▹ $ts) $p ↪ $q $t (λ x, quantₙ $q $ts ($p x)); symbol ∀ₙ [n] ≔ @quantₙ @∀ n; symbol ∃ₙ [n] ≔ @quantₙ @∃ n; -// Tests +// tests private symbol f1 : Endo 4 o; @@ -119,29 +105,29 @@ private opaque symbol ex_cong a b c d x y w z : π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (f1 a b c d = f1 x y w z) ≔ begin assume a b c d x y w z heq1 heq2 heq3 heq4; - refine refl_cong (o ▹ o ▹ o ▹ o ▹ unit) f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 + refine refl_cong (o ▹ o ▹ o ▹ o ▹ ◃) f1 _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 end; private opaque symbol ex_cong_param a b c d x y w z - (g : Fun (o ▹ o ▹ o ▹ o ▹ unit) o) : + (g : Fun (o ▹ o ▹ o ▹ o ▹ ◃) o) : π (a = x) → π (b = y) → π (c = w) → π (d = z) → π (g a b c d = g x y w z) ≔ begin assume a b c d x y w z g heq1 heq2 heq3 heq4; - refine refl_cong (o ▹ o ▹ o ▹ o ▹ unit) g _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 + refine refl_cong (o ▹ o ▹ o ▹ o ▹ ◃) g _ _ heq1 _ _ heq2 _ _ heq3 _ _ heq4 end; private opaque symbol ex_cong_add (a b x y : ℕ) : π (a = x) → π (b = y) → π (a + b = x + y) ≔ begin assume a b x y h1 h2; - refine refl_cong (nat ▹ nat ▹ unit) (+) _ _ h1 _ _ h2 + refine refl_cong (nat ▹ nat ▹ ◃) (+) _ _ h1 _ _ h2 end; -assert x y ⊢ let u ≔ comp (nat ▹ unit) (+) (+1) in u x y ≡ x + (y +1); +assert x y ⊢ let u ≔ comp (nat ▹ ◃) (+) (+1) in u x y ≡ x + (y +1); -private opaque symbol testSubst (p: Fun (nat ▹ nat ▹ unit) o) a b x y: +private opaque symbol testSubst (p: Fun (nat ▹ nat ▹ ◃) o) a b x y: π (a = x) → π (b = y) → π (p a b) → π (p x y) ≔ begin assume p a b x y ax by; - refine refl_subst (nat ▹ nat ▹ unit) p _ _ ax _ _ by + refine refl_subst (nat ▹ nat ▹ ◃) p _ _ ax _ _ by end; From 3b5bd11b197a47c6700b1633a91b782c04c44b18 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 25 Sep 2026 08:37:21 +0200 Subject: [PATCH 6/6] update CHANGES [no ci] --- CHANGES.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 14f115a..76f9e9c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -5,6 +5,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/). ## Unreleased +### Added + +- Pos: builtins for parsing decimal numbers +- Univ: universe levels for Set and Prop +- NaryFun: n-ary functions and relations + ### Changed - Changed rewrite rules to be in line with the Rocq standard library.