search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

Tactics for emptyEquiv #7

Closed Ayertienna closed 11 years ago

Ayertienna commented 12 years ago

We may want to automate proofs for emptyEquiv in label-free since they all seem to follow similar patterns.

Ayertienna commented 12 years ago

This is partially done in emptyEquivLib.v, but no automation and no proofs of the library lemmas are provided.

ETA: mid Sept?

Ayertienna commented 11 years ago

I think it's enough for now; another full review (and possibly automation) of all the proofs will be done eventually, as needed