Commit cfccb191 authored by Raphael Cauderlier's avatar Raphael Cauderlier

[fol] n-ary connectives

parent 21a02708
......@@ -91,6 +91,13 @@ def make_fun : As : types -> A : type -> (fun_arrs As A) -> function.
(; Formulae ;)
prop : Type.
(; Lists of props are only used as intermediary step for building n-ary connectives ;)
props : Type.
nil_prop : props.
cons_prop : prop -> props -> props.
def snoc_prop : props -> prop -> props.
[A] snoc_prop nil_prop A --> cons_prop A nil_prop
[As,A,B] snoc_prop (cons_prop A As) B --> cons_prop A (snoc_prop As B).
(; Connectives ;)
false : prop.
......@@ -105,7 +112,52 @@ def not (p : prop) := imp p false.
def true := not false.
def eqv (p : prop) (q : prop) := and (imp p q) (imp q p).
(; n-ary quantification ;)
(; n-ary connectives ;)
def nand_list : props -> prop.
[] nand_list nil_prop --> true
[A] nand_list (cons_prop A nil_prop) --> A
[A1,A2,As] nand_list (cons_prop A1 (cons_prop A2 nil_prop))
--> and A1 (nand_list (cons_prop A2 nil_prop)).
(; nand_type n == propⁿ -> prop ;)
def nand_type : nat -> Type.
[] nand_type nat.O --> prop
[n] nand_type (nat.S n) --> prop -> nand_type n.
(; nand_aux [B₁; …; Bₘ] n A₁ … Aₙ == nand_list [B₁; …; Bₘ; A₁; …; Aₙ]
== B₁ ∧ … ∧ Bₘ ∧ A₁ ∧ … ∧ Aₙ ;)
def nand_aux : props -> n : nat -> nand_type n.
[Bs] nand_aux Bs nat.O --> nand_list Bs
[Bs,n] nand_aux Bs (nat.S n) --> A => nand_aux (snoc_prop Bs A) n.
def nand : n : nat -> nand_type n := nand_aux nil_prop.
def nor_list : props -> prop.
[] nor_list nil_prop --> false
[A] nor_list (cons_prop A nil_prop) --> A
[A1,A2,As] nor_list (cons_prop A1 (cons_prop A2 nil_prop))
--> or A1 (nor_list (cons_prop A2 nil_prop)).
def nor_aux : props -> n : nat -> nand_type n.
[Bs] nor_aux Bs nat.O --> nor_list Bs
[Bs,n] nor_aux Bs (nat.S n) --> A => nor_aux (snoc_prop Bs A) n.
def nor : n : nat -> nand_type n := nor_aux nil_prop.
def nimp_list : props -> prop -> prop.
[B] nimp_list nil_prop B --> B
[A,As,B] nimp_list (cons_prop A As) B --> imp A (nimp_list As B).
def nimp_aux : props -> n : nat -> nand_type (nat.S n).
[Bs] nimp_aux Bs nat.O --> A => nimp_list Bs A
[Bs,n] nimp_aux Bs (nat.S n) --> A => nimp_aux (snoc_prop Bs A) n.
def nimp : n : nat -> nand_type (nat.S n) := nimp_aux nil_prop.
(; nall n A₁ A₂ … Aₙ (a₁ : term A₁ => a₂ : term A₂ => … => aₙ : term Aₙ => P a₁ a₂ … aₙ)
==
all A₁ (a₁ : term A₁ => all A₂ (a₂ : term A₂ => … all Aₙ (aₙ : term Aₙ => P a₁ a₂ … aₙ)…)) ;)
(; nall_aux [A₁; …; Aₙ] : (term A₁ -> … -> term Aₙ -> prop) -> prop ;)
def nall_aux_type : types -> Type.
......
......@@ -171,9 +171,26 @@ are represented by Dedukti variables.
The universal and existential quantifiers are respectively =fol.all=
and =fol.ex=. They have the same Dedukti type: =A : fol.type -> (fol.term A -> fol.prop) -> fol.prop=.
For convenience, n-ary versions =fol.nall= and =fol.nex= of these
quantifiers are also defined. They have the same type =n : nat.Nat -> A₁ : type -> … -> Aₙ : type -> (term A₁ -> … -> term Aₙ -> prop) -> prop= and are defined by nesting =fol.all= and =fol.ex=.
**** n-ary connectives and quantifiers
For convenience, n-ary versions =fol.nand=, =fol.nor=, =fol.nimp=,
=fol.nall=, and =fol.nex= of respectively =fol.or=, =fol.and=,
=fol.imp=, =fol.all=, and =fol.ex= are also defined with the following
types:
- =fol.nand : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop=
- =fol.nor : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop=
- =fol.nimp : n : nat.Nat -> A₁ : prop -> … -> Aₙ : prop -> prop -> prop=
- =fol.nall : n : nat.Nat -> A₁ : type -> … -> Aₙ : type -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
- =fol.nex : n : nat.Nat -> A₁ : type -> … -> Aₙ : type -> (term A₁ -> … -> term Aₙ -> prop) -> prop=
They are defined by nesting the corresponding connectives and quantifiers as follows:
- =fol.nand 0 = fol.true=
- =fol.nand n A₁ A₂ … Aₙ = fol.and A₁ (fol.and A₂ (…Aₙ…))=
- =fol.nor 0 = fol.false=
- =fol.nor n A₁ A₂ … Aₙ = fol.or A₁ (fol.or A₂ (…Aₙ…))=
- =fol.imp n A₁ A₂ … Aₙ B = fol.imp A₁ (fol.imp A₂ (… (fol.imp Aₙ B)…))=
- =fol.nall n A₁ A₂ … Aₙ P = fol.all A₁ (a₁ : fol.term A₁ => fol.all A₂ (a₂ : fol.term A₂ => … fol.all Aₙ (aₙ : fol.term Aₙ => P a₁ … aₙ)…))=
- =fol.nex n A₁ A₂ … Aₙ P = fol.ex A₁ (a₁ : fol.term A₁ => fol.ex A₂ (a₂ : fol.term A₂ => … fol.ex Aₙ (aₙ : fol.term Aₙ => P a₁ … aₙ)…))=
*** Proofs
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment