feat(Tactic/ByContra): by_contra' tactic

[kbuzzard]

trafficstars

Implementation of by_contra'. Note that it needs the (as yet unimplemented) push_neg.

[kbuzzard]

I realised that I could implement the entire tactic in "tactic mode". Is that a bit hacky?

Issues I failed to deal with:

1. I would like to have better error reporting; if exact this fails on line 49 or 55 it would be helpful if the user sees an error saying "the negation of the goal is not push_neg-equivalent to the proposed type. But I don't know how to do that with my tactic mode hack.

2. Line 35 of tests: I create a nameless goal : \not P which I don't know how to delete.

[kbuzzard]

@dupuisf and Jireh Loreaux are porting push_neg and I think that it would be simpler to wait until that is done before merging this (I'll have to fix the tests anyway).

[kbuzzard]

The push_neg PR is #344.

[kbuzzard]

I tried to get this working, now push_neg has been merged, but apparently my code doesn't work any more, I don't know why, and unfortunately I don't have the time to think about this right now (I wrote this code in July whilst in the same room as Leo and since then have forgotten what little I knew about tactic writing; this is an exciting thing about being in your 50s when you learn something and then don't continue to practice it a lot).

[gebner]

Congratulations! You've found an exciting bug in push_neg! It was the usual missing instantiateMVars.

There's still one failing test, I'll let you fix it.

BTW, guard_hyp foo : ty works, only guard_hyp this : ty doesn't. The bug fix is in https://github.com/leanprover/std4/commit/7787697470956ebf7a74c6b76b387d2da08d0b5f but we still need to import std4 here.

[gebner]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build

[kbuzzard]

Oh thanks for the explanation and the fix Gabriel! I'm sorry I didn't finish the job, I don't usually look much at github and I only just now saw the notification.