search

ku-fpg / hermit-shell

HERMIT with GHCi shell
BSD 3-Clause "New" or "Revised" License
2 stars 0 forks source link

Should reflexivity look through foralls? #35

Closed andygill closed 8 years ago

andygill commented 8 years ago

I needed to replace

apply reflexivity

with

apply (anyTD reflexivity)

in the Hanoi example, because of the error message "reflexivity may only be applied to equivalence lemmas". 

Goal:
  ∀ △ l. l ≡ l
*** Exception: server failure: Object (fromList [("exception",String "no scope to end.")]) : no scope to end.

Should reflexivity look through foralls?

ecaustin commented 8 years ago

Logically speaking, no. You should have to skolemize that term before applying reflexivity. If we want to add a command that combines these steps I'm all for it, but it shouldn't be called reflexivity in my opinion.

On a related note, does anyTD reflexivity actually do what we think it does here? Is it reducing the term to forall l. l and HERMIT is recognizing that as a complete proof, or is anyTD promoting reflexivity's "success" to the top level? In other words, would anyTD reflexivity also work as a proof for something like forall l z. l = l && l = z?

xich commented 8 years ago

@andygill You should be able to just end-proof (or whatever the new shell equivalent is) here. More useful than calling reflexivity directly is simplify-proof and smash. reflexivity is meant to be more primitive. You certainly can apply it using anyTD if you want, but it shouldn't try to look through the foralls.

@ecaustin reflexivity rewrites an equivalence of the form e === e to true, so anyTD reflexivity in this case should give forall t l. true... at which point you can simplify away the foralls. The only case HERMIT considers a complete proof is when the lemma is reduced to true... though the end-proof command runs simplify-proof for you... wish just iterates reflexivity and elimination rules, so you don't usually have to go that far.

xich commented 8 years ago

Many of the proof commands still look through foralls, but I think as a design principle we should move away from this to work at a single intended level (like reflexivity does) and then promote/traverse/target with kure strategies. I'm actually working on doing this cleanup now... though I basically get to look at HERMIT on Saturdays, so it might be another week or two.

andygill commented 8 years ago

I should have the hermit-shell working, with travis builds, and the tests working, before the end of this weekend. This should help a bit.

andygill commented 8 years ago

Closing. reflexivity is a primitive that does not look through foralls.