Search code examples
proofidris

Idris: Proving some contradiction cases


I am new to Idris and Proofs in general but I am progressing through Software Foundations ported to Idris. I am working on an exercise

namespace Booleans

  data Bool = True | False

  andb : Booleans.Bool -> Booleans.Bool  -> Booleans.Bool
  andb True b = b
  andb False _ = False

  orb : Booleans.Bool -> Booleans.Bool -> Booleans.Bool
  orb True _ = True
  orb False b = b

  (&&) : Booleans.Bool -> Booleans.Bool  -> Booleans.Bool
  (&&) = andb

  (||) : Booleans.Bool -> Booleans.Bool  -> Booleans.Bool
  (||) = orb

  andb_eq_orb : (b, c : Booleans.Bool) -> (b && c = b || c) -> b = c

there are obviously four cases and two hold for reflexivity.

  andb_eq_orb True True _ = Refl
  andb_eq_orb True False prf = ?rhs1
  andb_eq_orb False True prf = ?rhs2
  andb_eq_orb False False _ = Refl

Checking the holes reveals

Main.Booleans.rhs1
    prf : True && False = True || False
---------------------------------
Main.Booleans.rhs1 : True = False

Main.Booleans.rhs2
    prf : False && True = False || True
---------------------------------
Main.Booleans.rhs2 : False = True

I don't understand that while the assertions are obviuosly illogical that is what I need to prove for those two steps. I don't see any rewrite steps I could make. More but abstractly I dont understand the approach or pattern to solve this either logically or explicitly in the langauge (Idris).


I am able to get both of the approaches to work by implementing the Uninhabbited interface for the type signature as such:

Uninhabited (Booleans.True && Booleans.False = Booleans.True || Booleans.False) where
    uninhabited Refl impossible

Solution

  • I'm not sure how did you define && and || and why they don't reduce for you, so let me show how this would work for stdlib Bool:

    If you write the following:

    andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
    andb_eq_orb True  True  _   = Refl
    andb_eq_orb True  False prf = ?rhs1
    andb_eq_orb False True  prf = ?rhs2
    andb_eq_orb False False _   = Refl
    

    then

    > :t rhs1
    prf : False = True
    --------------------------------------
    rhs1 : True = False
    Holes: Booleans.rhs2, Booleans.rhs1
    
     > :t rhs2
    prf : False = True
    --------------------------------------
    rhs2 : False = True
    

    One way you could fill this would be simply by passing through these reduced proofs, swapping the sides where necessary:

    andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
    andb_eq_orb True  True  _   = Refl
    andb_eq_orb True  False prf = sym prf
    andb_eq_orb False True  prf = prf
    andb_eq_orb False False _   = Refl
    

    Another, proper way to do this would be to use the Uninhabited interface, which gives you a proof of Void given a contradictory premise. You can then use a void : Void -> a function (aka the principle of explosion), or a convenient synonym absurd = void . uninhabited:

    andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
    andb_eq_orb True  True  _   = Refl
    andb_eq_orb True  False prf = absurd prf
    andb_eq_orb False True  prf = absurd prf
    andb_eq_orb False False _   = Refl