patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-10 06:08:39 +00:00
Code Issues Packages Projects Releases Wiki Activity

Move the tautology stuff (#107)

Browse Source
This commit is contained in:
Patrick Stevens
2020-04-05 19:27:59 +01:00
committed by GitHub
parent 2f07a8e972
commit f5bac0c091
3 changed files with 28 additions and 50 deletions
Download Patch File Download Diff File Expand all files Collapse all files

25
Logic/PropositionalAxiomsTautology.agda
View File

@@ -9,3 +9,28 @@ open import Vectors
module Logic.PropositionalAxiomsTautology where
axiomKTaut : {a : _} {A : Set a} (P Q : Propositions A) → Tautology (implies P (implies Q P))
axiomKTaut P Q v with inspect (Valuation.v v P)
axiomKTaut P Q v | BoolTrue with≡ pT with inspect (Valuation.v v Q)
axiomKTaut P Q v | BoolTrue with≡ pT | BoolTrue with≡ qT = Valuation.vImplicationT v (Valuation.vImplicationT v pT)
axiomKTaut P Q v | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v qF)
axiomKTaut P Q v | BoolFalse with≡ pF = Valuation.vImplicationVacuous v pF
axiomSTaut : {a : _} {A : Set a} (P Q R : Propositions A) → Tautology (implies (implies P (implies Q R)) (implies (implies P Q) (implies P R)))
axiomSTaut P Q R v with inspect (Valuation.v v P)
axiomSTaut P Q R v | BoolTrue with≡ pT with inspect (Valuation.v v Q)
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolTrue with≡ qT with inspect (Valuation.v v R)
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolTrue with≡ rT = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationT v rT))
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolFalse with≡ rF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT (Valuation.vImplicationF v qT rF))
axiomSTaut P Q R v | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT qF))
axiomSTaut P Q R v | BoolFalse with≡ pF = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationVacuous v pF))
excludedMiddleTaut : {a : _} {A : Set a} (P : Propositions A) → Tautology (implies (prNot (prNot P)) P)
excludedMiddleTaut P v with inspect (Valuation.v v P)
excludedMiddleTaut P v | BoolTrue with≡ pT = Valuation.vImplicationT v pT
excludedMiddleTaut P v | BoolFalse with≡ pF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v (Valuation.vImplicationVacuous v pF) (Valuation.vFalse v))
propositionalAxiomsTautology : {a : _} {A : Set a} (x : Sg ThreeElements (indexAxiom A)) → Tautology (IsSubset.ofElt propositionalAxioms x)
propositionalAxiomsTautology (One , (fst ,, snd)) = axiomKTaut fst snd
propositionalAxiomsTautology (Two , record { one = one ; two = two ; three = three }) = axiomSTaut one two three
propositionalAxiomsTautology (Three , b) = excludedMiddleTaut b

28
Logic/PropositionalLogic.agda
View File

@@ -81,7 +81,7 @@ valuationsAreFree : {a : _} {pr : Set a} → (w : pr → Bool) → {x : pr} →
valuationsAreFree w = refl
Tautology : {a : _} {pr : Set a} (prop : Propositions pr) → Set a
Tautology {pr = pr} prop = {v : Valuation pr} → Valuation.v v prop ≡ BoolTrue
Tautology {pr = pr} prop = (v : Valuation pr) → Valuation.v v prop ≡ BoolTrue
record IsSubset {a b : _} (sub : Set a) (super : Set b) : Set (a ⊔ b) where
field
@@ -216,32 +216,6 @@ deductionTheorem {P = P} {Q} record { n = n ; proof = (nextStep .n proof (modusP
-}
axiomKTaut : {a : _} {A : Set a} {P Q : Propositions A} → Tautology (implies P (implies Q P))
Tautology.isTaut (axiomKTaut {P = P} {Q}) {v = v} with inspect (Valuation.v v P)
Tautology.isTaut (axiomKTaut {P = P} {Q}) {v} | BoolTrue with≡ pT with inspect (Valuation.v v Q)
Tautology.isTaut (axiomKTaut {P = P} {Q}) {v} | BoolTrue with≡ pT | BoolTrue with≡ qT = Valuation.vImplicationT v (Valuation.vImplicationT v pT)
Tautology.isTaut (axiomKTaut {P = P} {Q}) {v} | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v qF)
Tautology.isTaut (axiomKTaut {P = P} {Q}) {v} | BoolFalse with≡ pF = Valuation.vImplicationVacuous v pF
excludedMiddleTaut : {a : _} {A : Set a} {P : Propositions A} → Tautology (implies (prNot (prNot P)) P)
Tautology.isTaut (excludedMiddleTaut {P = P}) {v} with inspect (Valuation.v v P)
Tautology.isTaut (excludedMiddleTaut {P = P}) {v} | BoolTrue with≡ pT = Valuation.vImplicationT v pT
Tautology.isTaut (excludedMiddleTaut {P = P}) {v} | BoolFalse with≡ pF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v (Valuation.vImplicationVacuous v pF) (Valuation.vFalse v))
axiomSTaut : {a : _} {A : Set a} {P Q R : Propositions A} → Tautology (implies (implies P (implies Q R)) (implies (implies P Q) (implies P R)))
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} with inspect (Valuation.v v P)
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} | BoolTrue with≡ pT with inspect (Valuation.v v Q)
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} | BoolTrue with≡ pT | BoolTrue with≡ qT with inspect (Valuation.v v R)
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolTrue with≡ rT = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationT v rT))
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolFalse with≡ rF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT (Valuation.vImplicationF v qT rF))
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT qF))
Tautology.isTaut (axiomSTaut {P = P} {Q} {R}) {v} | BoolFalse with≡ pF = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationVacuous v pF))
propositionalAxiomsTautology : {a : _} {A : Set a} (x : Sg ThreeElements (indexAxiom A)) → Tautology (IsSubset.ofElt propositionalAxioms x)
propositionalAxiomsTautology (One , (fst ,, snd)) = axiomKTaut
propositionalAxiomsTautology (Two , record { one = one ; two = two ; three = three }) = axiomSTaut
propositionalAxiomsTautology (Three , b) = excludedMiddleTaut
propositionalLogicSound : {a b c : _} {A : Set a} {givens : Set c} {givensSubset : IsSubset givens (Propositions A)} → {P : Propositions A} → Proves propositionalAxioms givensSubset P → Entails givensSubset P
Entails.entails (propositionalLogicSound {P = .(IsSubset.ofElt propositionalAxioms x)} record { n = .0 ; proof = (nextStep .0 empty (axiom x)) ; ofStatement = refl }) {v} values = Tautology.isTaut (propositionalAxiomsTautology x) {v}

25
Logic/PropositionalLogicExamples.agda
View File

@@ -9,35 +9,14 @@ open import Vectors
module Logic.PropositionalLogicExamples where
axiomK : {a : _} {A : Set a} {P Q : Propositions A} → Tautology (implies P (implies Q P))
axiomK {P = P} {Q} {v = v} with inspect (Valuation.v v P)
axiomK {P = P} {Q} {v} | BoolTrue with≡ pT with inspect (Valuation.v v Q)
axiomK {P = P} {Q} {v} | BoolTrue with≡ pT | BoolTrue with≡ qT = Valuation.vImplicationT v (Valuation.vImplicationT v pT)
axiomK {P = P} {Q} {v} | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v qF)
axiomK {P = P} {Q} {v} | BoolFalse with≡ pF = Valuation.vImplicationVacuous v pF
excludedMiddle : {a : _} {A : Set a} {P : Propositions A} → Tautology (implies (prNot (prNot P)) P)
excludedMiddle {P = P} {v} with inspect (Valuation.v v P)
excludedMiddle {P = P} {v} | BoolTrue with≡ pT = Valuation.vImplicationT v pT
excludedMiddle {P = P} {v} | BoolFalse with≡ pF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v (Valuation.vImplicationVacuous v pF) (Valuation.vFalse v))
axiomS : {a : _} {A : Set a} {P Q R : Propositions A} → Tautology (implies (implies P (implies Q R)) (implies (implies P Q) (implies P R)))
axiomS {P = P} {Q} {R} {v} with inspect (Valuation.v v P)
axiomS {P = P} {Q} {R} {v} | BoolTrue with≡ pT with inspect (Valuation.v v Q)
axiomS {P = P} {Q} {R} {v} | BoolTrue with≡ pT | BoolTrue with≡ qT with inspect (Valuation.v v R)
axiomS {P = P} {Q} {R} {v} | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolTrue with≡ rT = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationT v rT))
axiomS {P = P} {Q} {R} {v} | BoolTrue with≡ pT | BoolTrue with≡ qT | BoolFalse with≡ rF = Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT (Valuation.vImplicationF v qT rF))
axiomS {P = P} {Q} {R} {v} | BoolTrue with≡ pT | BoolFalse with≡ qF = Valuation.vImplicationT v (Valuation.vImplicationVacuous v (Valuation.vImplicationF v pT qF))
axiomS {P = P} {Q} {R} {v} | BoolFalse with≡ pF = Valuation.vImplicationT v (Valuation.vImplicationT v (Valuation.vImplicationVacuous v pF))
emptySubset : {a : _} (A : Set a) → IsSubset False A
emptySubset A = record { ofElt = λ () }
emptyEntailment : {a b : _} {A : Set a} {P : Propositions A} → Entails (emptySubset (Propositions A)) P → Tautology P
emptyEntailment {a} {b} {A} {P} record { entails = entails } {v} = entails {v} λ {s} → exFalso s
emptyEntailment {a} {b} {A} {P} record { entails = entails } v = entails {v} λ {s} → exFalso s
emptyEntailment' : {a b : _} {A : Set a} {P : Propositions A} → Tautology P → Entails (emptySubset (Propositions A)) P
Entails.entails (emptyEntailment' isTaut) {v} _ = isTaut {v}
Entails.entails (emptyEntailment' isTaut) {v} _ = isTaut v
data TwoElements : Set where
One : TwoElements