Remove the tactic `auto_inj_pair2`

DeepSpec / InteractionTrees

A Library for Representing Recursive and Impure Programs in Coq

MIT License

199 stars 50 forks source link

Remove the tactic `auto_inj_pair2` #132

Closed gilhur closed 5 years ago

gilhur commented 5 years ago

I replaced inv by dependent destruction when the tactic auto_inj_pair2 is needed.

Lysxia commented 5 years ago

Fair enough.

That reminds me that it's possible to avoid axioms (which dependent destruction depends on) altogether in the itree library (by using eq_dep in the VisF rule of what is now eqit), but paco already uses JMeq_eq. Is there any way to make paco axiom-free as well?

gmalecha commented 5 years ago

I recall the idea of axiom-free paco being brought up a long time ago.

gilhur commented 5 years ago

Oh I forgot about the axiom issue. Here is a summary.

"JMeq_eq" is equivalent to UIP (Uniqueness of identity proof), which may be problematic in Homotopy Type Theory.
Paco uses "JMeq_eq" only for implementing the tactics. I guess it might be possible to implement them without using "JMeq_eq".
I already used "dependent destruction" in many places and that's why I removed "auto_inj_pair2".

But, since we may want to try to remove "JMeq_eq" later, let's keep the tactic "auto_inj_pair2".

I will close this pull request.

Lysxia commented 5 years ago

@gilhur auto_inj_pair2 also uses an axiom, so doesn't this PR still make sense to make the proofs more uniform?