The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi all,

Please consider following code:

Goal (forall n : nat, ~ (n >= 0) -> False) -> True.
  unfold not. fold not.

This code unfolded not, so the goal becomes

(forall n : nat, (n >= 0 -> False) -> False) -> True

But the next one fold not is not able to refold the not to turn the inner condition back to ~ (n >= 0).

In general, I tried to write code like this,

  intros.
  match goal with
  | [ _ : forall _, ?T |- _ ] =>
    idtac T
  end.

following the program above, in my Coq 8.6, it says no matching clause. But I suspect this error message is bogus, the real error should be Coq wouldn't allow us to capture a dependent right hand side of implication, due to the potential misuse of free variables. That probably also explains why fold cannot undo what unfold has done.

This is especially disturbing, when I do autounfold in *. There are many lemmas expressed with the presence of not, and if not is unfolded, auto family does not seem work well with that form anymore. Might I ask how do you guys handle it?

In general, is there a way to manipulate dependent rhs of implication?

Sincerely Yours,

Jason Hu