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

Termination checker got a bit sad on upgrade to Agda 2.6.1 (#103)

Browse Source
This commit is contained in:
Patrick Stevens
2020-03-28 18:10:55 +00:00
committed by GitHub
parent d2d1c4d3f2
commit 162a1c7a40
1 changed files with 10 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

17
Logic/PropositionalLogic.agda
View File

@@ -50,14 +50,17 @@ valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolTrue with≡ p |
valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolTrue with≡ p | BoolFalse with≡ q rewrite p | q | Valuation.vImplicationF v1 p q | Valuation.vImplicationF v2 (equalityCommutative eqX) (equalityCommutative eqY) = refl
valuationIsDetermined v1 v2 pr {implies x y} | eqX | eqY | BoolFalse with≡ p rewrite p | Valuation.vImplicationVacuous v1 {q = y} p | Valuation.vImplicationVacuous v2 {q = y} (equalityCommutative eqX) = refl
extendValuationV : {a : _} {pr : Set a} → (w : pr → Bool) → Propositions pr → Bool
extendValuationV w (ofPrimitive x) = w x
extendValuationV w false = BoolFalse
extendValuationV w (implies x y) with extendValuationV w x
... | BoolTrue with extendValuationV w y
extendValuationV w (implies x y) | BoolTrue | BoolTrue = BoolTrue
... | BoolFalse = BoolFalse
extendValuationV w (implies x y) | BoolFalse = BoolTrue
extendValuation : {a : _} {pr : Set a} → (w : pr → Bool) → Valuation pr
Valuation.v (extendValuation w) (ofPrimitive x) = w x
Valuation.v (extendValuation w) false = BoolFalse
Valuation.v (extendValuation w) (implies x y) with Valuation.v (extendValuation w) x
Valuation.v (extendValuation w) (implies x y) | BoolTrue with Valuation.v (extendValuation w) y
Valuation.v (extendValuation w) (implies x y) | BoolTrue | BoolTrue = BoolTrue
Valuation.v (extendValuation w) (implies x y) | BoolTrue | BoolFalse = BoolFalse
Valuation.v (extendValuation w) (implies x y) | BoolFalse = BoolTrue
Valuation.v (extendValuation w) = extendValuationV w
Valuation.vFalse (extendValuation w) = refl
Valuation.vImplicationF (extendValuation w) {p} {q} pT qF with Valuation.v (extendValuation w) p
Valuation.vImplicationF (extendValuation w) {p} {q} refl qF | BoolTrue with Valuation.v (extendValuation w) q