Able to prove two contradictory theorems

[Kazark]

I noticed there are a number of issues around the totality checker and impossible, but it is not obvious to me whether this is a dupe with any of them. This example seems simpler than some of what I saw there, and if it is a dupe I may need some guidance from people who understand the guts better than I do in knowing which ones to link it to.

The problem is that I am able to prove Args_str_map_exhaustive (for all TAction, lookup does not fail to find it in StrMap) with simply Refl impossible when as Args_str_map_not_exhaustive demonstrates, there is actually a counterexample (there exists a TAction--Teleport--which such that lookup fails to find it in the StrMap). When I try to construct the bogus theorem specific to Teleport (Teleport_in_list), Idris can see that it is bogus. I am also able to construct the counterexample proof more simply/directly in Teleport_not_in_list.

The following code compiles:

module TAction

%default total
%access public export

data TAction
  = Transmogrify
  | Teleport
  | Timetravel

Eq TAction where
  Transmogrify == Transmogrify = True
  Teleport == Teleport = True
  Timetravel == Timetravel = True
  _ == _ = False

StrMap : List (TAction, String)
StrMap =
  [ (Transmogrify, "transmogrify")
  , (Timetravel, "timetravel")
  ]

Args_str_map_exhaustive : Not (List.lookup a StrMap = Nothing)
Args_str_map_exhaustive Refl impossible

Args_str_map_not_exhaustive : (a : TAction ** List.lookup a StrMap = Nothing)
Args_str_map_not_exhaustive = (Teleport ** Refl)

-- Does not compile: "is a valid case"
--Teleport_in_list : Not (List.lookup Teleport StrMap = Nothing)
--Teleport_in_list Refl impossible

Teleport_not_in_list : List.lookup Teleport StrMap = Nothing
Teleport_not_in_list = Refl

I observed this both in 1.2.0 and 1.3.1.

[Kazark]

Perhaps I would be better off avoid the negation and forcing myself to prove the theorem in the positive. I went for the negative because I thought it would require less maintenance as I added cases. However, this does not compile, which is good:

Args_str_map_exhaustive : (a : TAction) -> (b : String ** List.lookup a StrMap = Just b)
Args_str_map_exhaustive Transmogrify = (_ ** Refl)
Args_str_map_exhaustive Teleport = (_ ** Refl) -- says Nothing doesn't equal Just
Args_str_map_exhaustive Timetravel = (_ ** Refl)

[Kazark]

EDIT: I screwed up. Ignore this stupid comment. In my own moving things back and forth I just screwed up the following code, so of course it compile. :fried_egg: -> :face_with_head_bandage:

--

Okay, I'm really on a roll today. I was able to to break even the positive statement of the proof. This compiles:

data Shape
  = Eel | Baboon | Bug | Calvin | Dinosaur | Elephant | Frog | Tiger | Toad
  | Worm

Eq Shape where
  Eel == Eel = True
  Baboon == Baboon = True
  Bug == Bug = True
  Calvin == Calvin = True
  Dinosaur == Dinosaur = True
  Elephant == Elephant = True
  Frog == Frog = True
  Tiger == Tiger = True
  Toad == Toad = True
  Worm == Worm = True
  _ == _ = False

data TAction
  = Transmogrify Shape
  | Teleport
  | Timetravel

Eq TAction where
  (Transmogrify s1) == (Transmogrify s2) = True
  Teleport == Teleport = True
  Timetravel == Timetravel = True
  _ == _ = False

StrMap : List (TAction, String)
StrMap =
  [ (Transmogrify Eel, "transmogrify")
  , (Teleport, "teleport")
  , (Timetravel, "timetravel")
  ]

Args_str_map_exhaustive : (a : TAction) -> (b : String ** List.lookup a StrMap = Just b)
Args_str_map_exhaustive (Transmogrify _) = (_ ** Refl)
Args_str_map_exhaustive Teleport = (_ ** Refl)
Args_str_map_exhaustive Timetravel = (_ ** Refl)

[Kazark]

This final result pretty much ruins Idris for me: I no longer have any sense of when I can trust it. I'm going to start learning Agda instead, I think, but I also see the problem before the Idris community: it is small, it is fringe, it is on the bleeding edge. Brady is trying to build 2.0, while 1.x is gaining traction and yet far from mature and stable. I care about this.

I have been trying hard to learn type theory, and not only type theory but how to implement actual languages with it. I would love to get to the place where I could help track down and fix this kind of stuff in Idris, but I don't know. I don't have tons of free time to work on stuff like this, but I do wish I knew how to get to the point where I could meaningfully contribute given the constraints of my poor knowledge and limited time.

[clayrat]

The first one does seem problematic, the coverage checker seems to ignore the fact that there's a parameter which can affect the reduction.

Your last example, however, is a valid program: List.lookup uses your Eq implementation, which ignores the parameter to Transmogrify. If you change the first case in that to (Transmogrify s1) == (Transmogrify s2) = s1 == s2, it will fail to compile, as expected.

[Kazark]

@clayrat Thanks so much for your response. I couldn't be more happy to be wrong. If very basic proof by pattern matching is restored that restores Idris to usability for me somewhat: if I at least have a knowledge of where to look out for trouble.

When I posted the initial stuff I was pretty careful and cross-checked myself a number of ways (thus the multiplication of different approaches). However apparently I got careless! My implicit trust in Idris having been taken away, I reverted into my number one problem, which is my implicit trust in myself. :tongue:

There was a version of my code where I had s1 == s2 (which is the whole reason there is an Eq Shape at all), but in all the changing things back and forth and trying things I screwed it up.

Anyway, glad to be wrong, and thanks for the response! I wish I could ask how one goes about tracking down and finding such a bug in the coverage checker, but I don't think I've even ever got Idris to compile, since my cabal knowledge is poor and it's a big complex program. :frowning_face: So, not sure where to start. I tried to make some minor contributions a while back, but they were either stupid (trying to add library functions before I had a clue, if I'm honest) or things where I didn't get far (trying to implement & as forward-pipe but couldn't compile to test my changes). But even recently I haven't been able to compile Idris.

The problem is it seems I need a background in Haskell tooling to start working on this, but in Haskell I have never got beyond toy projects using Stack instead of Cabal (I read about Haskell and look at its libraries constantly, so as I language I understand it reasonably well, but my ability to use the ecosystem is poor).

[clayrat]

@Kazark I've compiled it several times using the scripts at https://github.com/melted/get-idris/, maybe you could find some magic parameters in there that could help? My Haskell knowledge is pretty limited too, I'm afraid. Generally, problems like these is one of the reasons to become self-hosting, hence Blodwen ;)

[Kazark]

@clayrat Thanks, I'll have to give that a shot.

[Kazark]

Trying lots of different things to get Idris building both on Windows and Linux: cabal, stack, installing a new cabal, a new ghc... finally got a successful cabal install on Linux. Stack on Windows choking on pkg-config >= 0.9 when I do have 0.26 on my path. Working on adding a test with a repro of this problem.

[Kazark]

Not going to be able to red-green-refactor this; I don't know enough to know exactly what the error should look like once it's being produced. So, I'll set the test up to pass as it is now, and then try to break the test. Unconventional!

[Kazark]

I'm looking at mkPatTm in Coverage.hs. According to the description in the comments, it seems relevant. I'm wondering what exactly about my example broke it: Was it List.lookup? etc. Am going to experiment more.

[Kazark]

Inlining lookup and lookupBy into the same module do not change the effect. Introducing (a : TAction) -> explicitly in the type signature doesn't either. It's not until I actually case split on the introduced variable that the effect changes. Thus as far as I can tell this is not a particularly esoteric situation.

[Kazark]

What's the best way to go about understanding this code? Is it just to read it through in detail? I haven't found where I could write unit tests that would help me understand this case. Ideally I would really like to write a unit test that would help me understand which branch of the pattern match the function is going down. I'm struggling to understand what term is under question as the argument to mkPatTm. (Flailing here, obviously...)

[Kazark]

Okay, addImpl' looks like it adds implicit arguments. This doesn't seem to apply, since as I said above, when I made the implicit argument explicit, it didn't change the results. Hm, though. Aren't typeclasses a sort of implicit in Idris? I'm not sure. Makes me think I should test out what happens when I remove the Eq instance in the example and just used a plain equality function.

[Kazark]

Removing the Eq instance didn't have any effect. Going to move on from addImpl'.

[Kazark]

Hm, or should I be looking at the validCoverageCase function?

[Kazark]

Or checkPossible in Elab/Clause.hs? A pattern match in elabClause that is calling it makes it look like that might be the right track...

[Kazark]

Okay, I have a suspicion that the problem is this: Refl is impossible in two cases, possible in one: it is only taking into account one of the cases. So shouldn't the logic be, if Refl can be valid at all, then Refl is a valid case?---which is the message getting emitted by the clause of elabClause that I'm looking at (Clause.hs:648). If this is correct,, then checkPossible is indeed where I need to look, and I need to make sure it returns Just for this case.

[Kazark]

I see there is some sort of elaborator log by the logElab function. How does one make use of that? It could be very helpful to know which branch of logic I'm going down. I do think I'm in the right area in checkPossible but it's very thick: there's a lot to absorb and a lot that's unfamiliar.

[Kazark]

Interestingly, if I make the list empty, it is able to detect that Refl is a valid case. However, as long as the list is non-empty, it does not matter how many things I leave out of it.

[Kazark]

Posing the problem in terms of elemBy does not exhibit the problem. So is there something in the definition of elemBy versus lookupBy that is goofing us up?

Cases : List TAction
Cases = [Teleport]

Cases_Exhaustive : Not (List.elemBy (===) a Cases = False)
Cases_Exhaustive Refl impossible

^ Does not typecheck, saying Refl is a valid case, which is good.

Also, I found --log=10 on the command-line gives extreme verbose output.

[Kazark]

The only real difference between elemBy and lookupBy is the use of Bool versus Maybe, and that lookupBy has a let in it.

||| Check if something is a member of a list using a custom comparison.
elemBy : %static (a -> a -> Bool) -> a -> List a -> Bool
elemBy p e []      = False
elemBy p e (x::xs) =
  if p e x then
    True
  else
    elemBy p e xs

||| Find associated information in a list using a custom comparison.
lookupBy : %static (a -> a -> Bool) -> a -> List (a, b) -> Maybe b
lookupBy p e []      = Nothing
lookupBy p e (x::xs) =
  let (l, r) = x in
    if p e l then
      Just r
    else
      lookupBy p e xs

However, when I match out (l, r) in the main pattern match instead of using let, it has no effect on the outcome.

After playing with many, many variations of this, it seems that the problem is Maybe versus Bool. I do not find this enlightening.

[Kazark]

It really does have something to do with Bool versus Maybe. Even this does not compile (i.e. it does not exhibit the bug):

Str_map_exhaustive : (a : TAction) -> Not (isJust (List.lookup a StrMap) = False)
Str_map_exhaustive x Refl impossible

[Kazark]

This also does not compile. Again, though, I am not enlightened.

data IsNothing : Maybe a -> Type where
  ItIsNothing : IsNothing Nothing

Str_map_exhaustive : (a : TAction) -> Not (IsNothing (List.lookup a StrMap))
Str_map_exhaustive x Refl impossible

[Kazark]

Trying to parse through the logs, I am quite overwhelmed and don't know what to make of them. I am though intrigued that this also exhibits the bug:

Str_map_exhaustive : (a : TAction) -> Not (List.lookup a StrMap = Nothing)
Str_map_exhaustive Transmogrify Refl impossible
Str_map_exhaustive x Refl impossible

This is particularly interesting, because I'm working with stripped down version of the type in this example, that only has Transmogrify and Teleport, so x in the second match can only be Teleport. If only Idris realized this, it would know that case was not impossible.

[Kazark]

I'm in way over my head here. Anybody care to throw me a rope? I could use some help. I would like to be of use here and fix this if I can but I'm floundering.

[melted]

Thanks for the research.

I’ll take a look at it.

6 nov. 2018 kl. 06:40 skrev Keith Pinson notifications@github.com:

I'm in way over my head here. Anybody care to throw me a rope? I could use some help. I would like to be of use here and fix this if I can but I'm floundering.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or mute the thread.

[Kazark]

@melted Thanks so much. Let me know if I can be of use.