idris-lang / Idris-dev

A Dependently Typed Functional Programming Language
http://idris-lang.org
Other
3.44k stars 644 forks source link

Invalid case-split resulting in impossible #3587

Open jachymb opened 7 years ago

jachymb commented 7 years ago

I am trying prove the following simple statement:

multEqTrans : (a:Nat) -> (b:Nat) -> (c:Nat) -> (d:Nat) -> a * b = c -> b = d -> a * d = c

I ask Idris for body skeleton and get:

multEqTrans : (a:Nat) -> (b:Nat) -> (c:Nat) -> (d:Nat) -> a * b = c -> b = d -> a * d = c
multEqTrans a b c d prf prf1 = ?multEqTrans_rhs

OK, then I case split on prf and get:

multEqTrans : (a:Nat) -> (b:Nat) -> (c:Nat) -> (d:Nat) -> a * b = c -> b = d -> a * d = c
multEqTrans a b (a * b) d Refl prf1 = ?multEqTrans_rhs_1

Sill OK, but then I case split again on prf1 and get:

multEqTrans : (a:Nat) -> (b:Nat) -> (c:Nat) -> (d:Nat) -> a * b = c -> b = d -> a * d = c
multEqTrans _ _ (_ * _) _ Refl Refl impossible

Which is nonsense. Idris actually knows there is some problem, because I get this error when reloading:

multEqTrans _ _ (_ * _) _ Refl Refl is a valid case

By the way, here is a valid proof that type-checks:

total
multEqTrans : (a:Nat) -> (b:Nat) -> (c:Nat) -> (d:Nat) -> a * b = c -> b = d -> a * d = c
multEqTrans a b (a * b) d Refl prf1 = rewrite prf1 in Refl

I am using idris 0.99. This could perhaps be related to #2821 but I am not sure.

xekoukou commented 7 years ago

I think that the problem is that having Refl in the second proof does not update the types/values of the previous arguments.

It would a very nice feature to have that. Till then, it will confuse people.

In agda, this works :

module mult where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

multEqTrans : (a b c d : ℕ) → a * b ≡ c → b ≡ d → a * d ≡ c
multEqTrans a b .(a * b) .b refl refl = refl
ahmadsalim commented 7 years ago

I agree with @xekoukou that having this in Idris would be nice as well.

xekoukou commented 7 years ago

Here is another example :

test : Nat -> String
test x with (x)
  test Z | Z = ?dfs_3
  test (S x) | Z = ?dfs_4
  test Z | (S y) = ?dfs_1
  test (S x) | (S y) = ?dfs_5
ikervagyok commented 7 years ago

I'm new to Idris (just working my way through "Type-Driven Development with Idris"), but I seem to be stumbling across the same error when trying to create an append function on some simple trees:

data Tree : {length : Nat} -> (elem : Type) -> Type where
  Nil : Tree {length = 0} elem
  App : Tree {length = lengthL} elem -> elem -> Tree {length = lengthR} elem -> Tree {length = S (lengthL + lengthR)} elem

append : Tree {length = lengthL} elem -> Tree {length = lengthR} elem -> Tree {length = lengthL + lengthR} elem
append [] [] = []
append [] (App x y z) = App x y z
append (App x z w) y = ?append_rhs_2

and the REPL gives me this (after ditching atom, as i thought it was the editors fault):

*Test> :r
Type checking ./Test.idr
Holes: Test.append_rhs_2
*Test> :cs! 24 y
Holes: Test.append_rhs_2
*Test> :r
Type checking ./Test.idr
Test.idr:24:8:append (App _ _ _) [] is a valid case
Holes: Test.append

Is there any progress on this? Is there a way even a beginner to Idris could help?

ahmadsalim commented 7 years ago

@ikervagyok Unfortunately, there is no progress yet.

ahmadsalim commented 7 years ago

If you are interested in helping, you can take a look at the file src/Idris/CaseSplit.hs. You are welcome to use IRC or the mailing list if you are stuck somewhere.