Prop Solver

PropSolver.agda

open import Cubical.Data.Bool
open import Cubical.Data.Unit
open import Cubical.Foundations.Prelude
open import Cubical.Data.Sigma
open import Cubical.Data.Sum
open import Cubical.Foundations.HLevels
open import Cubical.Functions.Logic
open import Cubical.Foundations.Structure
open import Cubical.HITs.PropositionalTruncation 

module src.Data.InhabitedPropSolver where
    
    record Inhabited (A : Set): Set where 
        constructor inhab
        field 
            default : A

        
    open Inhabited {{...}}

    instance 
        topInhabited : Inhabited (Lift Unit)
        topInhabited = record { default = tt* }

        andInhabited : 
            {P Q : Set}
            {{ _ : Inhabited P}}
            {{ _ : Inhabited Q }} 
            → Inhabited ( P × Q)
        andInhabited = record { default = default , default}

        impInhabited : 
            {P Q : Set}
            {{ _ : Inhabited P}}
            {{ _ : Inhabited Q }} 
            → Inhabited ( P → Q)
        impInhabited = record { default = λ x → default }
        
        truncInhabited : { P : Set} → {{ _ : Inhabited P}} → Inhabited ( ∥ P ∥₁ )
        truncInhabited = record { default = ∣ default ∣₁ }

        sumLInhabited : { P Q : Set} → {{ _ : Inhabited P}} → Inhabited ( P ⊎ Q )
        sumLInhabited = record { default = _⊎_.inl default }
        
        -- {-# OVERLAPS sumRInhabited  #-}
        -- need to use something like this to guide resolution search, overlapping at sum
        -- sumRInhabited : { P Q : Set} → {{ _ : Inhabited Q}} → Inhabited ( P ⊎ Q )
        -- sumRInhabited = record { default = _⊎_.inr default }
        
        -- good luck defining this
        -- forallInhabited : {P : Set}{Q : P → Set}{{ _ : Inhabited P}} → Inhabited (∀ (x : P) → Q x)
        -- forallInhabited = {!   !}

    solve : {P Q : hProp ℓ-zero } {{ _ : Inhabited ⟨ P ⟩ }}{{ _ : Inhabited ⟨ Q ⟩ }} → P ≡ Q 
    solve = ⇔toPath default default

    module _
        {P Q R : hProp ℓ-zero }
        {{ _ : Inhabited ⟨ P ⟩ }}
        {{ _ : Inhabited ⟨ Q ⟩ }}
        {{ _ : Inhabited ⟨ R ⟩ }} where

        _ : P ⊓ Q ≡ Q ⊓ P
        _ = solve

        _ : ⊤ {ℓ-zero} ⊓ P ≡ P
        _ = solve
        
        _ : P ⊔ P ≡ P 
        _ = solve
        
        _ : P ⊔ (Q ⊓ R) ≡ (P ⊔ Q) ⊓ (P ⊔ R)
        _ = solve

        _ : P ⊔ ⊥ ≡ P
        _ = solve

        _ : P ⊔ (Q ⊔ R) ≡ (P ⊔ Q) ⊔ R 
        _ = solve

        _ : P ⇒ (Q ⊓ R) ≡ (P ⇒ Q) ⊓ (P ⇒ R) 
        _ = solve
        
        instance
            myPropInhabited : Inhabited ⟨ 1 ≡ₚ 1 ⟩ 
            myPropInhabited = inhab ∣ refl ∣₁

        _ : P ⊔ (1 ≡ₚ 1 ⊔ R) ≡ (P ⊔ Q) ⊔ 1 ≡ₚ 1  
        _ = solve