Strange behavior on Vacuous Quantification.

[chaosape]

First off, thanks for the tool!

I was playing around with logitext tonight and came across some strange behavior when unfolding a right implication introduction inference rule instance where the antecedent of the implication formula had an occurrence of vacuous quantification. Here is an example: http://logitext.mit.edu/proving/.28forall+y.2C+P+.2D.3E+Q.29+.2D.3E+P+.2D.3E+Q

[JasonGross]

My guess is that it's interpreting y as a variable of type Type, which I'm guessing it displays as U for universe. Note that all variables get the type "U".

[ezyang]

Heh, yes, this looks like a bug! I guess I'll have to jigger back functions involving universes back into their quantified versions.

[JasonGross]

This is a bit tricky (unless you're manually recording names), because even Set Printing All doesn't give you their names. Here's an 8.5-only way of doing it:

Ltac idtac_name x T := idtac x ":" T.
Ltac idtac_names T :=
  lazymatch T with
  | forall UNNAMED : ?A, ?P
    => idtac_name UNNAMED A;
       let ret := constr:(fun UNNAMED : A => match P with
                                             | v => ltac:(let v' := eval unfold v in v in idtac_names v'; exact I)
                                             end) in
       idtac
  | _ => idtac T
  end.
Goal forall P Q : Prop, (forall y : Prop, P -> Q) -> P -> Q.
  intros P Q H.
  let T := type of H in idtac_names T.

[jasonhemann]

I just ran into the same or a similar issue:

http://logitext.mit.edu/proving/.28forall+z.2C+.28forall+y.2C+.28A+.5C.2F+.7EA.29.29.29