Syntax experiment for propositional reasoning in cubical agda

logic.agda

{-# OPTIONS --cubical #-}
{-

This module shows a few syntactical additions, that, like Setoid reasoning in the standard library,
are supposed to make logical reasoning more readable. One of the goals is to avoid having to write
`PropositionalTruncation.rec squash` everywhere when "unpacking" a truncated datatype.

`obtain n ∶ A by prf - cont` does just that. It takes a "proof" producing a truncated ∥ A ∥ and
makes an untruncated A available in the context of cont. There is a special version for mere existance
of an element with a certain property making the property available as a "tactic":

`obtain x having P as n by prf - cont` where `prf` demonstrates `∃[ x ] P x`. I'm not so sure if this
version is as useful. Personally, I replaced all usages with the above in the end.

Record matching on telescopes on the obtained identifier `n` is possible, although currently it's connected to a bug
that shows weird names in interactive mode: https://github.com/agda/agda/issues/4599

-}
module logic where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Logic as L
open import Cubical.HITs.PropositionalTruncation as P

private
  variable
    ℓ ℓ' ℓ'' : Level

-- datatype declaration needed for the type checker to figure out proofs for (isProp P)
data ProofOf (P : hProp ℓ) : Type ℓ where
  proofOf : [ P ] → ProofOf P
isPropProofOf : {P : hProp ℓ} → isProp (ProofOf P)
isPropProofOf {P = P} (proofOf x) (proofOf y) i = proofOf (P .snd x y i)

infix 1 proof_by_
proof_by_ : (P : hProp ℓ) → ProofOf P → [ P ]
proof _ by (proofOf p) = p

infix 40 _qed
_qed : {P : Type ℓ} → P → P
p qed = p

exact_ : {P : hProp ℓ} → [ P ] → ProofOf P
exact_ = proofOf

have-syntax : (P : hProp ℓ) {Q : hProp ℓ'} (f : [ P ] → ProofOf Q) → ProofOf P → ProofOf Q
have-syntax _ f (proofOf x) = f x

syntax have-syntax P (λ x → cont) prf = have x ∶ P by prf - cont

obtain-syntax : {A : Type ℓ'} (P : A → hProp ℓ) {Q : hProp ℓ''} → (f : Σ[ x ∈ A ] ProofOf (P x) → ProofOf Q) → ProofOf (∃[ x ] P x) → ProofOf Q
obtain-syntax {A = A} P {Q = Q} f (proofOf x) = P.rec isPropProofOf (λ { (x , p) → f (x , proofOf p) }) x

syntax obtain-syntax (λ x → P) (λ n → cont) prf = obtain x having P as n by prf - cont

obtain-syntax2 : (A : Type ℓ) {Q : hProp ℓ'} → (f : A → ProofOf Q) → ProofOf ∥ A ∥ₚ → ProofOf Q
obtain-syntax2 _ {Q = Q} f (proofOf x) = P.rec isPropProofOf f x

syntax obtain-syntax2 A (λ n → cont) tac = obtain n ∶ A by tac - cont

private
  open import Cubical.Data.Nat
  input : [ ∃[ n ∶ ℕ ] n ≡ₚ 0 ]
  input = ∣ 0 , ∣ refl ∣ ∣

  want : _
  want =
    proof ∃[ n ∶ ℕ ] n ≡ₚ 2 by
       obtain n having n ≡ₚ 0 as (n , eq0) by exact input -
       obtain prf ∶ n ≡ 0 by eq0 -
       -- next could be written in one line, but I want to show that one can use let blocks and "have" syntax
       let n2 : [ ∃[ n ∶ ℕ ] n ≡ₚ 2 ]
           n2 = ∣ suc (suc n) , ∣ cong (λ x → suc (suc x)) prf ∣ ∣ in
       -- alternatively:
       have n2′ ∶ ∃[ n ∶ ℕ ] n ≡ₚ 2 by exact n2 -
       exact n2′
    qed

{-
Another application, although I don't want to include all the dependencies here, so it wouldn't typecheck. I hope it
shows that these sort of proofs can be readable:

Assume the following two functions, which should be familiar from ZF set theory

union-ax : [ ∀[ x ∶ V ℓ ] ∀[ u ] (u ∈ₛ ⋃ x ⇔ (∃[ v ] (v ∈ₛ x) ⊓ (u ∈ₛ v))) ]
replacement-ax : [ ∀[ r ∶ (V ℓ → V ℓ) ] ∀[ a ] ∀[ y ] (y ∈ₛ ⁅ r ∣ a ⁆ ⇔ (∃[ z ] (z ∈ₛ a) ⊓ (y ≡ₛ r z))) ]

cartesian-el : [ ∀[ A ∶ V ℓ ] ∀[ B ] ∀[ y ] (y ∈ₛ (A ⊗ B) ⇔ (∃[ a ] ∃[ b ] (a ∈ₛ A) ⊓ (b ∈ₛ B) ⊓ (y ≡ₛ ⁅ a , b ⁆o))) ]
cartesian-el A B y = forward , backward where
  stage2 : V _ → V _
  stage2 b = ⁅ ⁅_, b ⁆o ∣ A ⁆ 
  stage1 : V _
  stage1 = ⁅ stage2 ∣ B ⁆

  open import logic
  -- with excessive type annotations, but most of it can be deduced (see backwards block)
  forward : [ y ∈ₛ (A ⊗ B) ⇒ (∃[ a ] ∃[ b ] (a ∈ₛ A) ⊓ (b ∈ₛ B) ⊓ (y ≡ₛ ⁅ a , b ⁆o)) ]
  forward y∈AB =
    proof (∃[ a ] ∃[ b ] (a ∈ₛ A) ⊓ (b ∈ₛ B) ⊓ (y ≡ₛ ⁅ a , b ⁆o)) by
      obtain (z , z1 , yz) ∶ Σ[ z ∈ _ ] [ (z ∈ₛ stage1) ⊓ (y ∈ₛ z) ]
        by exact (union-ax stage1 y .fst y∈AB) -
      obtain (b , bB , yB) ∶ Σ[ b ∈ _ ] [ (b ∈ₛ B) ⊓ (z ≡ₛ stage2 b) ]
        by exact (replacement-ax stage2 B z .fst z1) -
      obtain (a , aA , yAB) ∶ Σ[ a ∈ _ ] [ (a ∈ₛ A) ⊓ (y ≡ₛ ⁅ a , b ⁆o) ]
        by exact (replacement-ax ⁅_, b ⁆o A y .fst (subst (λ z → [ y ∈ₛ z ]) yB yz)) -
      exact ∣ a , ∣ b , aA , bB , yAB ∣ ∣
    qed

  backward : [ (∃[ a ] ∃[ b ] (a ∈ₛ A) ⊓ (b ∈ₛ B) ⊓ (y ≡ₛ ⁅ a , b ⁆o)) ⇒ y ∈ₛ (A ⊗ B) ]
  backward aby =
    proof y ∈ₛ (A ⊗ B) by
      obtain (a , exb) ∶ _ by exact aby -
      obtain (b , aA , bB , yAB) ∶ _ by exact exb -
      have a2 ∶ y ∈ₛ stage2 b
        by (exact (replacement-ax ⁅_, b ⁆o A y .snd ∣ a , aA , yAB ∣)) -
      have b2 ∶ stage2 b ∈ₛ stage1
        by (exact (replacement-ax stage2 B (stage2 b) .snd ∣ b , bB , refl ∣)) -
      exact (union-ax stage1 y .snd ∣ stage2 b , b2 , a2 ∣)
    qed
-}