-- Examples
-- Here are some complete sample programs.
-- Written for Agda1/OldSyntax by Catarina Coquand.
-- Modified for Agda1/NewSyntax by Yoshiki Kinoshita.
id (A::Set) (!x::A) :: A = x
Pred (!A::Set) :: Type = A -> Set
Rel (!A::Set) :: Type = A -> A -> Set
(*) (!A,!B::Set) :: Set = sig {fst::A; snd::B}
prod (A,B::Set) (!a::A) (!b::B) :: A*B
= struct fst :: A = a
snd :: B = b
reflexive (A::Set) (!R::Rel A) :: Set = (x::A) -> (x `R` x)
symmetrical (A::Set) (!R::Rel A) :: Set = (x,y::A) -> x `R` y -> y `R` x
transitive (A::Set) (!R::Rel A) :: Set = (x,y,z::A) -> x `R` y -> y `R` z -> x `R` z
substitutive (A::Set) (!R::Rel A) :: Type
= (x,y::A) -> x `R` y -> (P::Pred A) -> (P x -> P y) * (P y -> P x)
EqRel (!A::Set) :: Type
= sig R :: Rel A
refl :: reflexive R
sym :: symmetrical R
trans :: transitive R
lemma1 (!A::Set)
(!S::Rel A)
(!s::substitutive S)
(!r::reflexive S) :: EqRel A =
let s' :: symmetrical S =
\ (x,y :: A) ->
\ (h :: (x `S` y)) ->
let P :: Pred A = \(z :: A) -> z `S` x
lem :: (x `S` x) -> (y `S` x) = (s x y h P).fst
in lem (r x)
t :: transitive S =
\(x,y,z::A) ->
\(h::x `S` y) ->
\(h'::y `S` z) ->
let P :: Pred A = \(x::A) -> x `S` z
lem :: (y `S` z) -> (x `S` z) = (s x y h P).snd
in lem h'
in struct R :: Rel A = S
refl :: reflexive R = r
sym :: symmetrical R = s'
trans :: transitive R = t
EqRelProd (A, B::Set) (!eq1::EqRel A)(!eq2::EqRel B) :: EqRel (A * B) =
let ProdC :: Set = A*B
P (!p1,!p2::ProdC) :: Set = eq1.R p1.fst p2.fst
Q (!p1,!p2::ProdC) :: Set = eq2.R p1.snd p2.snd
T :: Rel ProdC = \ (p1,p2 :: ProdC) -> (p1 `P` p2)*(p1 `Q` p2)
lem1 :: reflexive T =
\ (z::ProdC) ->
struct fst :: z `P` z = eq1.refl z.fst
snd :: z `Q` z = eq2.refl z.snd
lem2 :: symmetrical T =
\ (x, y::ProdC) -> \ (h:: x `T` y) ->
struct fst :: y `P` x = eq1.sym x.fst y.fst h.fst
snd :: y `Q` x = eq2.sym x.snd y.snd h.snd
lem3 :: transitive T =
\ (x, y, z::ProdC) ->
\ (h1::x `T` y) -> \ (h2::y `T` z) ->
struct fst :: x `P` z = eq1.trans x.fst y.fst z.fst h1.fst h2.fst
snd :: x `Q` z = eq2.trans x.snd y.snd z.snd h1.snd h2.snd
in struct R::Rel ProdC = T
refl::reflexive T = lem1
sym::symmetrical R = lem2
trans::transitive R = lem3
data Nat = Z | S (n::Nat)
data N1 = TT
true :: N1 = TT
data N0 =
absElim (!h::N0) (!A::Set) :: A = case h of {}
zero :: Nat = Z
succ :: Nat -> Nat = S
Vec (!A::Set) (!n::Nat) :: Set
= case n of
(Z )-> A
(S n')-> Vec A n' * A
EqRelVec (A::Set) (!eq::EqRel A) (!k::Nat) :: EqRel (Vec A k)
= case k of
(Z )-> eq
(S n)-> EqRelProd (EqRelVec eq n) eq
(==) :: Rel Nat
= \(m,n::Nat) -> case m of
(Z )-> case n of
(Z )-> N1
(S n')-> N0
(S m')-> case n of
(Z )-> N0
(S n')-> m' == n'
substEqNat :: substitutive (==)
= \(x,y::Nat)
-> \(h::x == y)
-> \(P::Pred Nat)
-> case x of
(Z )-> case y of
(Z )-> struct fst :: P Z -> P Z = id
snd :: P Z -> P Z = id
(S y')-> struct fst :: P x -> P y = absElim h (P Z -> P (S y'))
snd :: P y -> P x = absElim h (P (S y') -> P Z)
(S x')-> case y of
(Z )-> struct fst :: P x -> P y = absElim h (P (S x') -> P Z)
snd :: P y -> P x = absElim h (P Z -> P (S x'))
(S y')-> let Q :: Pred Nat = \(n::Nat) -> P (S n)
in substEqNat x' y' h Q
EqRelNat :: EqRel Nat
= let reflexiveEqNat :: reflexive (==)
= \(x::Nat) -> case x of
(Z )-> true
(S n)-> reflexiveEqNat n
in lemma1 Nat (==) substEqNat reflexiveEqNat
EqRelVecNat :: (k::Nat) -> EqRel (Vec Nat k) = EqRelVec EqRelNat
mutual {
data U = n
| pi (x::U) (y::T x -> U)
T (!x :: U) :: Set = case x of
(n ) -> Nat
(pi x' y') -> (b::T x') -> T (y' b)
}
{-
Another example is a formaliztion of a completeness for a restricted subset
of intuitionistic logic with respect to Kripke semantics. There are holes
in proofs that are left as exercises.
(This is actually an exercise in a logic course given at the department.)
-}
-- Completeness for a restricted subset of intuitionistic logic with respect to
-- Kripke semantics.
-- Below we prove completness for intuitionistic propositional logic restricted
-- to implication and conjunction, i.e. no disjunction.
-- After having defined some basic notions of relations we define the logic that we
-- will use by giving its formulas and rules. After havind proved some derived rule
-- we define the semantics of the logic. We conculde the lab by proving soundness
-- and completeness.
-- It is your assignment to fill in the missing parts of the proof!
-- When doing formal proofs using a proof editor there is a constant temptation to
-- start hackng on the proof before having a clear understanding of it. Sometimes
-- such random hacking can be a way to get aquainted with the theorem to be proved,
-- but most often it leads to only frustartion and meaningless proof terms. If you
-- get stuck go for a walk or take a cup of coffee and try to make a mental picture
-- of the proof before going back to the formalism.
-- The introduction of the manual to another formal proof system, Isabelle, starts
-- with the following citation which is worth contemplating. It is from Chesterton,
-- The man who was orthodox:
-- You can only find truth with logic
-- if you have already found truth without it.
-- We first define some basic notions used throughout this lab (and in
-- mathematics).
and (!A,!B :: Set) :: Set = sig {fst :: A; snd :: B}
imply (!A,!B :: Set) :: Set = A ->B
(<-->) (!A,!B :: Set) :: Set = (A->B) `and` (B->A)
pred (!S :: Set) :: Type = (x :: S) -> Set {- A predicate -}
rel (!S :: Set) :: Type = (s1,s2 :: S) -> Set {- A relation -}
mirror (S :: Set) (!R :: rel S) :: rel S = \(x,y :: S) -> y `R` x
-- Below is a collection of properties of relations, i.e. transitivity,
-- reflexivity and the definition of poset.
package RelationTheory (S :: Set) ((<=) :: rel S) where
trans :: Set = (x,y,z :: S) -> (p :: x <= y) -> (q :: y <= z) -> x <= z
ref :: Set = (x :: S) -> x <= x
poset :: Set =
sig
isref :: ref
istrans :: trans
-- We collect some definitions and lemmas related to posets.
package PosetTheory (S :: Set) ((<=) :: rel S)
(aPoset :: (RelationTheory S (<=)).poset) where
open aPoset use posetIsRef = isref, posetIsTrans = istrans
-- A predicate P is upward closed (sometimes called monotone) if it holds for an
-- element x then it holds also for all elements larger than x.
upwClosed (!P :: pred S) :: Set = (x,y :: S) -> (p :: P x) -> (xlty :: x<=y) -> P y
-- We can now define the type of all upward closed predicates
-- (we have to use Type to avoid a Russel style of paradox)
upwClosedPred :: Type =
sig
aPred :: pred S
isUpwClosed :: upwClosed aPred
(>) :: rel S = mirror (<=)
open RelationTheory S (>)
use mirrorTrans = trans, mirrorRef = ref, mirrorPoset = poset
-- We now define a function "bar" that takes an arbitary predicate P as
-- argument and returns a predicate that cuts down P minimally to make
-- it upward closed. It is your assignment to prove that this is the case!
bar (!P :: pred S) :: upwClosedPred =
struct
aPred :: pred S = \(x :: S) -> (y :: S) -> (xlty :: x <= y) -> P y
{- that is aPred is true for x if P is true for all y greater than x -}
isUpwClosed :: upwClosed aPred = ?
-- It is now time to define the logic for which we prove soundness and
-- completeness. It is propositional intuitionistic logic without disjunction
-- and absurdity. The formulas should be self explanatory.
package logic (ID :: Set) where
data Formula =
Atom (id :: ID)
| (->>) (f1 :: Formula) (f2 :: Formula)
| (/\) (f1 :: Formula) (f2 :: Formula)
-- We now give the rules that define the turnstyle relation, written F1 |- F2.
-- A relation is a deduction relation if it satisfies the rules given below
-- and is the smallest such relation.
-- This is an example of an inductively defined relation.
-- In the book "|-" is defined between a set of formulas and a formula.
-- To simplify things we use just one formula on the left instead of a set of formulas.
-- In this way we also get finite sets since a finite set of formulas on the left of
-- "|-" can be replaced by the conjunction of the formulas in the set.
DedRelIntro (!(|-) :: rel Formula) :: Set =
sig
andElim1 :: (f1, f2 :: Formula) -> (f1 /\ f2) |- f1
andElim2 :: (f1, f2 :: Formula) -> (f1 /\ f2) |- f2
andIntro :: (f1, f2, f3 :: Formula) -> (ass1 :: f1 |- f2) ->
(ass2 :: f1 |- f3) -> f1 |- (f2 /\ f3)
mp :: (f1, f2, f3 :: Formula) -> (ass1 :: f1 |- f2) ->
(ass2 :: f1 |- (f2 ->> f3)) -> f1 |- f3
arrowIntro :: (f1, f2, f3 :: Formula) -> (ass1 :: (f1 /\ f2) |- f3) ->
f1 |- (f2 ->> f3)
assumption :: (f1 :: Formula) -> f1 |- f1
weakeningLeft :: (f1, f2, f3 :: Formula) -> (ass1 :: f1 |- f2) ->
(f3 /\ f1) |- f2
-- The deduction relation we really want is the smallest one satisfying
-- the rules above. We formalise this below.
-- Notice that the isLeast condition can be read in two ways.
-- 1, For any other relation C that obeys the rules it should be the case
-- that for arbitrary formulas "f1" and "f2" if they hold for |- then they
-- should hold for C. And since C is arbitrary this means that |- is the smallest
-- possible relation that obeys the rules.
-- 2. We can also read the "isLeast" condition as a elimination rule
-- (or induction rule) for the turnstyle relation.
-- In that case we read "C" as an arbitrary condition on pairs of formulas.
DedRel (!(|-) :: rel Formula) :: Type =
sig
isDedRel :: DedRelIntro (|-)
isLeast :: (C :: rel Formula) -> (isDedRel :: DedRelIntro C) ->
(f1,f2 :: Formula) -> (holds :: f1 |- f2) -> C f1 f2
-- We (or rather you for some of them) now prove some simple derived rules.
-- This both serves as a test that we have not made any mistake in the rules
-- above and as a set of lemmas that simplifies the proof below.
package DerivedRules ((|-) :: rel Formula)
(isDedRel :: DedRelIntro (|-)) where
open isDedRel use
andElim1,andElim2,andIntro,mp,arrowIntro,assumption,weakeningLeft
cut (f1,f2,f3 :: Formula)
(!ass1 :: f1 |- f2)
(!ass2 :: f2 |- f3) :: f1 |- f3 =
isDedRel.mp f1 f2 f3 ass1 (isDedRel.arrowIntro f1 f2 f3
(isDedRel.weakeningLeft f2 f3 f1 ass2))
weakeningRight (!f1,!f2,!f3 :: Formula)
(!ass1 :: f1 |- f2) ::
(f1 /\ f3) |- f2 = ?
andLemma1 (f1,f2,f3 :: Formula)
(!ass1 :: f1 |- (f2 /\ f3)) :: f1 |- f2 =
cut ass1 (weakeningRight f2 f2 f3 (isDedRel.assumption f2))
andLemma2 (f1, f2, f3 :: Formula)(!ass1 :: f1 |- (f2 /\ f3))
:: f1 |- f3 =
cut ass1 (isDedRel.weakeningLeft f3 f3 f2 (isDedRel.assumption f3))
-- Here we define a Kripke model for a set of identifers as a tuple of a poset
-- and an assignment functions from identifers to upward closed predicates.
-- See van Dalen p. 164 for a discussion of the intuition regarding a creative
-- subject who understands (finds out the truth of) more and more about the
-- world as time goes by. He also never forgets anything;
-- his is assured for identifiers, since the predicate is
-- upward closed. For other formulas it should be proved.
kripkeModel (!S :: Set) :: Type =
sig
(<=) :: rel S
PS :: (RelationTheory S (<=)).poset
assign :: (id :: ID) -> (PosetTheory S (<=) PS).upwClosedPred
-- We are now ready to define what it means to interpret a formula in a
-- Kripke model.
-- We define ||-,
-- We also prove that somehting can be deduced then it is a consequence, i.e.
-- if f1 |- f2 then f1 ||- f2. This is soundness.
-- We collect the results in a theory.
package KripkeTheory (S :: Set) (km :: kripkeModel S) where
open km use (<=),PS,assign
open PosetTheory S (<=) PS use upwClosedPred, bar
-- at is used as a convenience below
at (S :: Set)(!f :: Set -> Set -> Set)
(!P1, !P2 :: pred S) :: pred S =
\ (x :: S) -> f (P1 x) (P2 x)
-- The interpretation of a conjunction is the conjunction of its parts.
-- To prove that it is upward closed is left to you.
conjInterpret (!P1 :: upwClosedPred)(!P2 :: upwClosedPred)
:: upwClosedPred =
struct
aPred :: pred S = at and P1.aPred P2.aPred
isUpwClosed :: (PosetTheory S (<=) PS).upwClosed aPred = ?
-- A ->> B is true at a point if B is true at any point in the future where A
-- is true.
implyInterpret (!P1 :: upwClosedPred)(!P2 :: upwClosedPred)
:: upwClosedPred =
bar (at imply P1.aPred P2.aPred)
interpret (!f :: Formula) :: upwClosedPred =
case f of
(Atom id) -> assign id
(f1 ->> f2) -> implyInterpret (interpret f1) (interpret f2)
(f1 /\ f2) -> conjInterpret (interpret f1) (interpret f2)
-- the semantics of a formula is thus a predicate over S
sem (!f :: Formula) :: pred S = (interpret f).aPred
-- We can now give the definition of consequence
-- F1 ||- F2 if we can prove (in the meta logic) that the interpretation of F2 is
-- true whenever the interpretation of F1 is true.
(||-) :: rel Formula =
\(F1, F2 :: Formula) ->
(x :: S) -> imply (sem F1 x) (sem F2 x)
-- We now prove soundness by proving that all rules are true when we choose the
-- deduction relation to be ||-
-- Since a well defined deduction relation is the smallest such relation we
-- then have soundness.
conseqIntro :: DedRelIntro (||-) =
struct
andElim1 :: (f1,f2 :: Formula) -> f1 /\ f2 ||- f1 =
\(f1,f2 :: Formula) ->
\(x :: S) ->
\(ass :: sem (f1 /\ f2) x) -> ass.fst
andElim2 :: (f1, f2 :: Formula) -> f1 /\ f2 ||- f2 = ?
andIntro :: (f1, f2, f3 :: Formula) -> (ass1 :: f1 ||- f2) -> (ass2 :: f1 ||- f3)
-> f1 ||- (f2 /\ f3) =
\(f1, f2, f3 :: Formula) ->
\(ass1 :: f1 ||- f2) ->
\(ass2 :: f1 ||- f3) ->
\(x :: S) ->
\(ass :: sem f1 x) ->
struct
fst :: sem f2 x =
ass1 x ass
snd :: sem f3 x =
ass2 x ass
mp :: (f1, f2, f3 :: Formula)
-> (ass1 :: f1 ||- f2)
-> (ass2 :: f1 ||- (f2 ->> f3))
-> f1 ||- f3 = ?
arrowIntro :: (f1, f2, f3 :: Formula)
-> (ass1 :: (f1 /\ f2) ||- f3)
-> f1 ||- (f2 ->> f3) = ?
assumption :: (f1 :: Formula) -> f1 ||- f1 =
\(f1 :: Formula) ->
\(x :: S) ->
\(ass :: sem f1 x) ->
ass
weakeningLeft :: (f1, f2, f3 :: Formula)
-> (ass1 :: f1 ||- f2)
-> (f3 /\ f1) ||- f2 =
\(f1, f2, f3 :: Formula) ->
\(ass1 :: f1 ||- f2) ->
\(x :: S) ->
\(ass :: sem (f3 /\ f1) x) ->
ass1 x ass.snd
-- We now come to the part of the lab when things become a bit involved.
-- We can now make a model where the points are formulas and the <= relation is
-- constructed from the |- relation.
-- The trickiest thing is to define a meaningful assignment function in this model.
-- Contempleate it!!
smallModel ((|-) :: rel Formula)
(!wd :: DedRel (|-)) :: kripkeModel Formula =
{-
open wd.isDedRel use andElim1, andElim2, andIntro, mp,arrowIntro, assumption , weakeningLeft in
open DerivedRules (|-) wd.isDedRel use cut, weakeningRight, andLemma1, andLemma2 in
open RelationTheory Formula (mirror Formula (|-)) use poset, ref, trans in
-}
struct
(<=) :: rel Formula = mirror (|-)
PS :: (RelationTheory Formula (mirror (|-))).poset =
struct isref :: (RelationTheory Formula (mirror (|-))).ref = (wd.isDedRel).assumption
istrans :: (RelationTheory Formula (mirror (|-))).trans =
\(x, y, z :: Formula) ->
\(p :: x <= y) ->
\(q :: y <= z) ->
(DerivedRules (|-) wd.isDedRel).cut q p
assign :: (id :: ID) -> (PosetTheory Formula (<=) PS).upwClosedPred =
\(id :: ID) ->
struct
aPred :: pred Formula =
\(x :: Formula) -> x |- Atom id
isUpwClosed :: (x, y :: Formula)
-> (p :: aPred x)
-> (xlty :: (x <= y))
-> aPred y = ?
-- And now we have finally arrived to the main theorem of the lab - the
-- completeness result.
package completenessTheory ((|-) :: rel Formula) (wd :: DedRel (|-)) where
aSmallModel :: kripkeModel Formula = smallModel wd
open aSmallModel use (<=)
open KripkeTheory Formula aSmallModel use interpret,sem,(||-)
open wd.isDedRel use andElim1, andElim2, andIntro, mp, arrowIntro, assumption, weakeningLeft
open DerivedRules (|-) wd.isDedRel use cut, weakeningRight, andLemma1, andLemma2
-- The lemma below is proved by induction over the formula f1.
-- This shows up as recursion in the proof object (program).
-- You have to check manually that the induction is proper, i.e. the recursive
-- applications of lemma is always to smaller elements.
lemma (!f1, !f2 :: Formula) :: sem f1 f2 <--> (f2 |- f1) =
case f1 of
(Atom id) ->
struct
fst :: (isTrue :: sem f1 f2) -> f2 |- f1 = \(isTrue :: sem f1 f2) -> isTrue
snd :: (isProvable :: f2 |- f1) -> sem f1 f2 = \(isProvable :: f2 |- f1) -> isProvable
(f1' ->> f2') -> ?
(f1' /\ f2') ->
struct
fst :: (isTrue :: sem (f1' /\ f2') f2) -> f2 |- (f1' /\ f2') =
\(isTrue :: sem (f1' /\ f2') f2) ->
andIntro f2 f1' f2'
((lemma f1' f2).fst isTrue.fst)
((lemma f2' f2).fst isTrue.snd)
snd :: (isProvable :: f2 |- (f1' /\ f2')) -> sem (f1' /\ f2') f2 =
\(isProvable :: f2 |- (f1' /\ f2')) ->
struct
fst :: sem f1' f2 =
(lemma f1' f2).snd (andLemma1 isProvable)
snd :: sem f2' f2 =
(lemma f2' f2).snd (andLemma2 isProvable)
-- And now completeness is trivial to prove!
complete (f1, f2 :: Formula)
(isConseq :: f1 ||- f2)
:: f1 |- f2 = ?