CODEWITHSUNDEEP
proofidris
akaphenom
akaphenom

Reputation: 6888

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

Upvotes: 0

Views: 245

Answers (1)

Alexander Gryzlov
Alexander Gryzlov

Reputation: 933

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

Upvotes: 1

Related Questions