Experimenting with code from https://github.com/avigad/lamr
https://avigad.github.io/lamr/using_lean_as_a_programming_language.html
2 +2: Nat22: Nat-55: Int[1,1: Nat2,2: Nat3]3: Nat#[1,1: Nat2,2: Nat3]3: NatArrayArray: Type u → Type u(1,1: Nat2,2: Nat3)3: Nat"hello world""hello world": Stringtruetrue: Boolfunx =>x: Natx +x: Nat11: Natλx =>x: Natx +x: Nat22: Natfunx => ifx: Natx =x: Nat1 then1: Nat"yes" else"yes": String"no""no": String([1,1: Nat2,2: Nat3] :3: NatListList: Type → TypeNat)Nat: Type(#[1,1: Nat2,2: Nat3] :3: NatArrayArray: Type → TypeNat) defNat: TypeisOne (isOne: Nat → Stringx :x: NatNat) :Nat: TypeString := ifString: Typex =x: Nat1 then1: Nat"yes" else"yes": String"no""no": StringisOneisOne: Nat → StringisOneisOne: Nat → String2 +2: Nat2 <2: Nat5 ∧5: NatisOneisOne: Nat → String3 =3: Nat"no" def"no": StringFermat_statement :Fermat_statement: PropProp := ∀Prop: Typeaa: Natbb: Natcc: Natn :n: NatNat,Nat: Typea *a: Natb *b: Natc ≠c: Nat0 ∧0: Natn >n: Nat2 →2: Nata^a: Natn +n: Natb^b: Natn ≠n: Natc^c: Natnn: NatFermat_statement theoremFermat_statement: Proptwo_plus_two_is_four :two_plus_two_is_four: 2 + 2 = 42 +2: Nat2 =2: Nat4 :=4: Natrfl theoremrfl: ∀ {α : Type} {a : α}, a = a:Fermat_statement :=Fermat_statement: Propsorrysorry: Fermat_statement
defprintExample :printExample: IO UnitIOIO: Type → TypeUnit:= doUnit: TypeIO.printlnIO.println: {α : Type} → [inst : ToString α] → α → IO Unit"hello""hello": StringIO.printlnIO.println: {α : Type} → [inst : ToString α] → α → IO Unit"world""world": StringprintExample defprintExample: IO Unitfactorial :factorial: Nat → NatNat →Nat: TypeNat |Nat: Type0 =>0: Nat1 | (1: Natn + 1) => (n: Natn +n: Nat1) *1: Natfactorialfactorial: Nat → Natnn: Natfactorialfactorial: Nat → Nat1010: Natfactorialfactorial: Nat → Nat100 def100: Nathanoi (hanoi: Nat → Nat → Nat → Nat → IO UnitnumPegsnumPegs: Natstartstart: Natfinishfinish: Nataux :aux: NatNat) :Nat: TypeIOIO: Type → TypeUnit := matchUnit: TypenumPegs with |numPegs: Nat0 =>0: Natpurepure: {f : Type → Type} → [self : Pure f] → {α : Type} → α → f α() |(): Unitn + 1 => don: Nathanoihanoi: Nat → Nat → Nat → Nat → IO Unitnn: Natstartstart: Natauxaux: Natfinishfinish: NatIO.println s!"Move disk {IO.println: {α : Type} → [inst : ToString α] → α → IO Unitn +n: Nat1} from peg {1: Natstart} to peg {start: Natfinish}"finish: Nathanoihanoi: Nat → Nat → Nat → Nat → IO Unitnn: Natauxaux: Natfinishfinish: Natstartstart: Nathanoihanoi: Nat → Nat → Nat → Nat → IO Unit77: Nat11: Nat22: Nat3 def3: NataddNums :addNums: List Nat → NatListList: Type → TypeNat →Nat: TypeNat | [] =>Nat: Type0 |0: Nata::a: Natas =>as: List Nata +a: NataddNumsaddNums: List Nat → Natasas: List NataddNums [addNums: List Nat → Nat0,0: Nat1,1: Nat2,2: Nat3,3: Nat4,4: Nat5,5: Nat6] section open List6: Natrangerange: Nat → List Nat77: NataddNums (addNums: List Nat → Natrangerange: Nat → List Nat7)7: NataddNums $addNums: List Nat → Natrangerange: Nat → List Nat77: Natmap (funmap: {α β : Type} → (α → β) → List α → List βx =>x: Natx +x: Nat3) $3: Natrangerange: Nat → List Nat77: Natmapmap: {α β : Type} → (α → β) → List α → List β(. + 3) $(. + 3): Nat → Natrangerange: Nat → List Nat77: Natfoldlfoldl: {α β : Type} → (α → β → α) → α → List β → α(. + .)(. + .): Nat → Nat → Nat0 $0: Natrangerange: Nat → List Nat77: Nat(. + .) end partial def(. + .): (x1 : ?m.3260) → (x2 : ?m.3268 x1) → ?m.3269 x1 x2gcdgcd: Nat → Nat → Natmm: Natn := ifn: Natn =n: Nat0 then0: Natm elsem: Natgcdgcd: Nat → Nat → Natn (n: Natm %m: Natn)n: Nat
section inductiveBinTree |BinTree: Typeempty :empty: BinTreeBinTree |BinTree: Typenode :node: BinTree → BinTree → BinTreeBinTree →BinTree: TypeBinTree →BinTree: TypeBinTree derivingBinTree: TypeRepr,Repr: Type u → Type uDecidableEq,DecidableEq: Sort u → Sort (max 1 u)Inhabited open BinTreeInhabited: Sort u → Sort (max 1 u)nodenode: BinTree → BinTree → BinTreeempty (empty: BinTreenodenode: BinTree → BinTree → BinTreeemptyempty: BinTreeempty) defempty: BinTreesize :size: BinTree → NatBinTree →BinTree: TypeNat |Nat: Typeempty =>empty: BinTree0 |0: Natnodenode: BinTree → BinTree → BinTreeaa: BinTreeb =>b: BinTree1 +1: Natsizesize: BinTree → Nata +a: BinTreesizesize: BinTree → Natb defb: BinTreedepth :depth: BinTree → NatBinTree →BinTree: TypeNat |Nat: Typeempty =>empty: BinTree0 |0: Natnodenode: BinTree → BinTree → BinTreeaa: BinTreeb =>b: BinTree1 +1: NatNat.max (Nat.max: Nat → Nat → Natdepthdepth: BinTree → Nata) (a: BinTreedepthdepth: BinTree → Natb) defb: BinTreeexample_tree :=example_tree: BinTreenode (node: BinTree → BinTree → BinTreenodenode: BinTree → BinTree → BinTreeemptyempty: BinTreeempty) (empty: BinTreenodenode: BinTree → BinTree → BinTreeempty (empty: BinTreenodenode: BinTree → BinTree → BinTreeemptyempty: BinTreeempty))empty: BinTreesizesize: BinTree → Natexample_treeexample_tree: BinTreedepthdepth: BinTree → Natexample_tree endexample_tree: BinTree
defisPrime (isPrime: Nat → Booln :n: NatNat) :Nat: TypeBool :=Bool: TypeId.run do ifId.run: {α : Type} → Id α → αn <n: Nat2 then2: Natfalse else forfalse: Booli in [i: Nat2:2: Natn] do ifn: Natn %n: Nati =i: Nat0 then return0: Natfalse iffalse: Booli *i: Nati >i: Natn then returnn: Nattruetrue: Booltruetrue: Bool(List.rangeList.range: Nat → List Nat10000).10000: Natfilterfilter: {α : Type} → (α → Bool) → List α → List αisPrime defisPrime: Nat → Boolprimes (primes: Nat → Array Natn :n: NatNat) :Nat: TypeArrayArray: Type → TypeNat :=Nat: TypeId.run do let mutId.run: {α : Type} → Id α → αresult :=result: Array Nat#[] for#[]: Array Nati in [i: Nat2:2: Natn] do ifn: NatisPrimeisPrime: Nat → Booli theni: Natresult :=result: Array Natresult.result: Array Natpushpush: {α : Type} → Array α → α → Array αii: Natresultresult: Array Nat(primesprimes: Nat → Array Nat10000).10000: Natsizesize: {α : Type} → Array α → Nat
https://avigad.github.io/lamr/implementing_propositional_logic.html
An atomic formula is a variable or one of the constants ⊤ or ⊥. A literal is an atomic formula or a negated atomic formula.
The set of propositional formulas in negation normal form (NNF) is generated inductively as follows:
Each literal is in negation normal form.
If A and B are in negation normal form, then so are A ∧ B and A ∨ B.
Proposition
Every propositional formula is equivalent to one in negation normal form.
Proof
First use the identities A ↔ B ≡ (A → B) ∧ (B → A) and A → B ≡ ¬A ∧ B to get rid of ≡ and →. Then use De Morgan’s laws together with ¬¬A ≡ A to push negations down to the atomic formulas.
section Props inductivePropForm |PropForm: Typetr :tr: PropFormPropForm |PropForm: Typefls :fls: PropFormPropForm |PropForm: Typevar :var: String → PropFormString →String: TypePropForm |PropForm: Typeconj :conj: PropForm → PropForm → PropFormPropForm →PropForm: TypePropForm →PropForm: TypePropForm |PropForm: Typedisj :disj: PropForm → PropForm → PropFormPropForm →PropForm: TypePropForm →PropForm: TypePropForm |PropForm: Typeimpl :impl: PropForm → PropForm → PropFormPropForm →PropForm: TypePropForm →PropForm: TypePropForm |PropForm: Typeneg :neg: PropForm → PropFormPropForm →PropForm: TypePropForm |PropForm: TypebiImpl :biImpl: PropForm → PropForm → PropFormPropForm →PropForm: TypePropForm →PropForm: TypePropForm derivingPropForm: TypeRepr,Repr: Type u → Type uDecidableEq open PropFormDecidableEq: Sort u → Sort (max 1 u)(impl (impl: PropForm → PropForm → PropFormconj (conj: PropForm → PropForm → PropFormvarvar: String → PropForm"p") ("p": Stringvarvar: String → PropForm"q")) ("q": Stringvarvar: String → PropForm"r")) namespace PropForm declare_syntax_cat propform syntax "prop!{""r": Stringpropform "}" :propform: Lean.Parser.Categoryterm syntax:max ident :term: Lean.Parser.Categorypropform syntax "⊤" :propform: Lean.Parser.Categorypropform syntax "⊥" :propform: Lean.Parser.Categorypropform syntax:35propform: Lean.Parser.Categorypropform:36 " ∧ "propform:36: Lean.Parser.Categorypropform:35 :propform: Lean.Parser.Categorypropform syntax:30propform: Lean.Parser.Categorypropform:31 " ∨ "propform:31: Lean.Parser.Categorypropform:30 :propform: Lean.Parser.Categorypropform syntax:20propform: Lean.Parser.Categorypropform:21 " → "propform:21: Lean.Parser.Categorypropform:20 :propform: Lean.Parser.Categorypropform syntax:20propform: Lean.Parser.Categorypropform:21 " ↔ "propform:21: Lean.Parser.Categorypropform:20 :propform: Lean.Parser.Categorypropform syntax:max "¬ "propform: Lean.Parser.Categorypropform:40 :propform: Lean.Parser.Categorypropform syntax:max "("propform: Lean.Parser.Categorypropform ")" :propform: Lean.Parser.Categorypropform macro_rules | `(prop!{$propform: Lean.Parser.Categoryp:ident}) => `(PropForm.var $(p: Lean.TSyntax `identLean.quoteLean.quote: {α : Type} → {k : optParam Lean.SyntaxNodeKind `term} → [self : Lean.Quote α k] → α → Lean.TSyntax kp.p: Lean.TSyntax `identgetId.getId: Lean.Ident → Lean.NametoString)) | `(prop!{⊤}) =>toString: Lean.Name → optParam Bool true → (optParam (String → Bool) fun x => false) → String`(ProfForm.tr) | `(prop!{⊥}) =>`(ProfForm.tr): Lean.MacroM Lean.Syntax`(ProfForm.fls) | `(prop!{¬ $`(ProfForm.fls): Lean.MacroM Lean.Syntaxp}) => `(PropForm.neg prop!{$p: Lean.TSyntax `propformp}) | `(prop!{$p: Lean.TSyntax `propformp ∧ $p: Lean.TSyntax `propformq}) => `(PropForm.conj prop!{$q: Lean.TSyntax `propformp} prop!{$p: Lean.TSyntax `propformq}) | `(prop!{$q: Lean.TSyntax `propformp ∨ $p: Lean.TSyntax `propformq}) => `(PropForm.disj prop!{$q: Lean.TSyntax `propformp} prop!{$p: Lean.TSyntax `propformq}) | `(prop!{$q: Lean.TSyntax `propformp → $p: Lean.TSyntax `propformq}) => `(PropForm.impl prop!{$q: Lean.TSyntax `propformp} prop!{$p: Lean.TSyntax `propformq}) | `(prop!{$q: Lean.TSyntax `propformp ↔ $p: Lean.TSyntax `propformq}) => `(PropForm.biImpl prop!{$q: Lean.TSyntax `propformp} prop!{$p: Lean.TSyntax `propformq}) | `(prop!{($q: Lean.TSyntax `propformp:p: Lean.TSyntax `propformpropform)}) => `(prop!{$propform: Lean.Parser.Categoryp}) private defp: Lean.TSyntax `propformtoString :toString: PropForm → StringPropForm →PropForm: TypeString |String: Typevarvar: String → PropForms =>s: Strings |s: Stringtr =>tr: PropForm"⊤" |"⊤": Stringfls =>fls: PropForm"⊥" |"⊥": Stringnegneg: PropForm → PropFormp => s!"(¬ {p: PropFormtoStringtoString: PropForm → Stringp})" |p: PropFormconjconj: PropForm → PropForm → PropFormpp: PropFormq => s!"({q: PropFormtoStringtoString: PropForm → Stringp} ∧ {p: PropFormtoStringtoString: PropForm → Stringq})" |q: PropFormdisjdisj: PropForm → PropForm → PropFormpp: PropFormq => s!"({q: PropFormtoStringtoString: PropForm → Stringp} ∨ {p: PropFormtoStringtoString: PropForm → Stringq})" |q: PropFormimplimpl: PropForm → PropForm → PropFormpp: PropFormq => s!"({q: PropFormtoStringtoString: PropForm → Stringp} → {p: PropFormtoStringtoString: PropForm → Stringq})" |q: PropFormbiImplbiImpl: PropForm → PropForm → PropFormpp: PropFormq => s!"({q: PropFormtoStringtoString: PropForm → Stringp} ↔ {p: PropFormtoStringtoString: PropForm → Stringq})"q: PropForminstance :instance: ToString PropFormToStringToString: Type → TypePropForm := ⟨PropForm: TypePropForm.toString⟩ end PropFormPropForm.toString: PropForm → Stringprop!{prop!{p ∧ q → (r ∨ ¬ p) → q}: PropFormp ∧ q → (r ∨ ¬ p) → q}prop!{p ∧ q → (r ∨ ¬ p) → q}: PropFormprop!{prop!{p ∧ q → (r ∨ ¬ p) → q}: PropFormp ∧ q → (r ∨ ¬ p) → q}prop!{p ∧ q → (r ∨ ¬ p) → q}: PropFormprop!{prop!{p ∧ q ∧ r → p}: PropFormp ∧ q ∧ r → p} defprop!{p ∧ q ∧ r → p}: PropFormpropExample :=propExample: PropFormprop!{prop!{p ∧ q → r ∧ p ∨ ¬ s1 → s2 }: PropFormp ∧ q → r ∧ p ∨ ¬ s1 → s2 }prop!{p ∧ q → r ∧ p ∨ ¬ s1 → s2 }: PropForm
Minimal enhancement for List related examples:
namespace List
def insert': {α : Type u_1} → [inst : DecidableEq α] → α → List α → List α
insert' [DecidableEq: Type u_1 → Type (max 0 u_1)
DecidableEq α: Type u_1
α] (a: α
a : α: Type u_1
α) (l: List α
l : List: Type u_1 → Type u_1
List α: Type u_1
α) : List: Type u_1 → Type u_1
List α: Type u_1
α :=
if a: α
a ∈ l: List α
l then l: List α
l else a: α
a :: l: List α
l
protected def union: {α : Type u_1} → [inst : DecidableEq α] → List α → List α → List α
union [DecidableEq: Type u_1 → Type (max 0 u_1)
DecidableEq α: Type u_1
α] (l₁: List α
l₁ l₂: List α
l₂ : List: Type u_1 → Type u_1
List α: Type u_1
α) : List: Type u_1 → Type u_1
List α: Type u_1
α :=
foldr: {α β : Type u_1} → (α → β → β) → β → List α → β
foldr insert': {α : Type u_1} → [inst : DecidableEq α] → α → List α → List α
insert' l₂: List α
l₂ l₁: List α
l₁
end List
namespace PropForm
def complexity: PropForm → Nat
complexity : PropForm: Type
PropForm → Nat: Type
Nat
| var: String → PropForm
var _ => 0: Nat
0
| tr: PropForm
tr => 0: Nat
0
| fls: PropForm
fls => 0: Nat
0
| neg: PropForm → PropForm
neg A: PropForm
A => complexity: PropForm → Nat
complexity A: PropForm
A + 1: Nat
1
| conj: PropForm → PropForm → PropForm
conj A: PropForm
A B: PropForm
B => complexity: PropForm → Nat
complexity A: PropForm
A + complexity: PropForm → Nat
complexity B: PropForm
B + 1: Nat
1
| disj: PropForm → PropForm → PropForm
disj A: PropForm
A B: PropForm
B => complexity: PropForm → Nat
complexity A: PropForm
A + complexity: PropForm → Nat
complexity B: PropForm
B + 1: Nat
1
| impl: PropForm → PropForm → PropForm
impl A: PropForm
A B: PropForm
B => complexity: PropForm → Nat
complexity A: PropForm
A + complexity: PropForm → Nat
complexity B: PropForm
B + 1: Nat
1
| biImpl: PropForm → PropForm → PropForm
biImpl A: PropForm
A B: PropForm
B => complexity: PropForm → Nat
complexity A: PropForm
A + complexity: PropForm → Nat
complexity B: PropForm
B + 1: Nat
1
def depth: PropForm → Nat
depth : PropForm: Type
PropForm → Nat: Type
Nat
| var: String → PropForm
var _ => 0: Nat
0
| tr: PropForm
tr => 0: Nat
0
| fls: PropForm
fls => 0: Nat
0
| neg: PropForm → PropForm
neg A: PropForm
A => depth: PropForm → Nat
depth A: PropForm
A + 1: Nat
1
| conj: PropForm → PropForm → PropForm
conj A: PropForm
A B: PropForm
B => Nat.max: Nat → Nat → Nat
Nat.max (depth: PropForm → Nat
depth A: PropForm
A) (depth: PropForm → Nat
depth B: PropForm
B) + 1: Nat
1
| disj: PropForm → PropForm → PropForm
disj A: PropForm
A B: PropForm
B => Nat.max: Nat → Nat → Nat
Nat.max (depth: PropForm → Nat
depth A: PropForm
A) (depth: PropForm → Nat
depth B: PropForm
B) + 1: Nat
1
| impl: PropForm → PropForm → PropForm
impl A: PropForm
A B: PropForm
B => Nat.max: Nat → Nat → Nat
Nat.max (depth: PropForm → Nat
depth A: PropForm
A) (depth: PropForm → Nat
depth B: PropForm
B) + 1: Nat
1
| biImpl: PropForm → PropForm → PropForm
biImpl A: PropForm
A B: PropForm
B => Nat.max: Nat → Nat → Nat
Nat.max (depth: PropForm → Nat
depth A: PropForm
A) (depth: PropForm → Nat
depth B: PropForm
B) + 1: Nat
1
def vars: PropForm → List String
vars : PropForm: Type
PropForm → List: Type → Type
List String: Type
String
| var: String → PropForm
var s: String
s => [s: String
s]
| tr: PropForm
tr => []: List String
[]
| fls: PropForm
fls => []: List String
[]
| neg: PropForm → PropForm
neg A: PropForm
A => vars: PropForm → List String
vars A: PropForm
A
| conj: PropForm → PropForm → PropForm
conj A: PropForm
A B: PropForm
B => (vars: PropForm → List String
vars A: PropForm
A).union: {α : Type} → [inst : DecidableEq α] → List α → List α → List α
union (vars: PropForm → List String
vars B: PropForm
B)
| disj: PropForm → PropForm → PropForm
disj A: PropForm
A B: PropForm
B => (vars: PropForm → List String
vars A: PropForm
A).union: {α : Type} → [inst : DecidableEq α] → List α → List α → List α
union (vars: PropForm → List String
vars B: PropForm
B)
| impl: PropForm → PropForm → PropForm
impl A: PropForm
A B: PropForm
B => (vars: PropForm → List String
vars A: PropForm
A).union: {α : Type} → [inst : DecidableEq α] → List α → List α → List α
union (vars: PropForm → List String
vars B: PropForm
B)
| biImpl: PropForm → PropForm → PropForm
biImpl A: PropForm
A B: PropForm
B => (vars: PropForm → List String
vars A: PropForm
A).union: {α : Type} → [inst : DecidableEq α] → List α → List α → List α
union (vars: PropForm → List String
vars B: PropForm
B)
end PropForm-- Minimal implementation for PropAssignment examples defPropAssignment :=PropAssignment: TypeList (List: Type → TypeString ×String: TypeBool) namespace PropAssignment defBool: Typemk (mk: List (String × Bool) → PropAssignmentvars :vars: List (String × Bool)List (List: Type → TypeString ×String: TypeBool)) :Bool: TypePropAssignment :=PropAssignment: Typevars defvars: List (String × Bool)eval? (eval?: PropAssignment → String → Option Boolτ :τ: PropAssignmentPropAssignment) (PropAssignment: Typevar :var: StringString) :String: TypeOptionOption: Type → TypeBool :=Bool: TypeId.run do letId.run: {α : Type} → Id α → ατ :τ: List (String × Bool)ListList: Type → Type_ :=_: Typeτ for (τ: PropAssignmentk,k: Stringv) inv: Boolτ do ifτ: List (String × Bool)k ==k: Stringvar then returnvar: Stringsomesome: {α : Type} → α → Option αv returnv: Boolnone defnone: {α : Type} → Option αeval (eval: PropAssignment → String → Boolτ :τ: PropAssignmentPropAssignment) (PropAssignment: Typevar :var: StringString) :String: TypeBool :=Bool: Typeτ.τ: PropAssignmenteval?eval?: PropAssignment → String → Option Boolvar |>.var: StringgetDgetD: {α : Type} → Option α → α → αfalse end PropAssignment deffalse: BoolPropForm.eval (PropForm.eval: PropAssignment → PropForm → Boolv :v: PropAssignmentPropAssignment) :PropAssignment: TypePropForm →PropForm: TypeBool |Bool: Typevarvar: String → PropForms =>s: Stringv.v: PropAssignmentevaleval: PropAssignment → String → Bools |s: Stringtr =>tr: PropFormtrue |true: Boolfls =>fls: PropFormfalse |false: Boolnegneg: PropForm → PropFormA => !(A: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentA) |A: PropFormconjconj: PropForm → PropForm → PropFormAA: PropFormB => (B: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentA) && (A: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentB) |B: PropFormdisjdisj: PropForm → PropForm → PropFormAA: PropFormB => (B: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentA) || (A: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentB) |B: PropFormimplimpl: PropForm → PropForm → PropFormAA: PropFormB => !(B: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentA) || (A: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentB) |B: PropFormbiImplbiImpl: PropForm → PropForm → PropFormAA: PropFormB => (!(B: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentA) || (A: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentB)) && (!(B: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentB) || (B: PropFormevaleval: PropAssignment → PropForm → Boolvv: PropAssignmentA))A: PropFormletv :=v: PropAssignmentPropAssignment.mk [(PropAssignment.mk: List (String × Bool) → PropAssignment"p","p": Stringtrue), (true: Bool"q","q": Stringtrue), (true: Bool"r","r": Stringtrue)]true: Boolprop!{prop!{p ∧ q ∧ r → p}: PropFormp ∧ q ∧ r → p}.prop!{p ∧ q ∧ r → p}: PropFormevaleval: PropAssignment → PropForm → Boolv end Propsv: PropAssignment