The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

Attached is a first attempt at a general-purpose "Prop smuggling" 
tactic: logicalize.  The point is to take a Prop hypothesis and "invert" 
it even when the current context is not Prop - producing a disjunction 
of exists terms, one for each constructor.

However, the JMeq's don't work in the result, as demonstrated in the 
second test.  Can anyone figure out what's going wrong?  If not, they 
can just be omitted.

Also needed is a way to simplify out false cases and factor out 
non-dependent parts from each exists term.

Jason: thanks for the "_ \/ _" hint!

-- Jonathan

Require Setoid JMeq.

(* on_last_hyp and rever_until copied from Coq.Program.Tactics *)

Ltac on_last_hyp tac :=
  match goal with [ H : _ |- _ ] => first [ tac H | fail 1 ] end.

Ltac revert_until id :=
  on_last_hyp ltac:(fun id' =>
    match id' with
      | id => idtac
      | _ => revert id' ; revert_until id
    end).

(* It's easiest to just wrap the results in exists: *)

Lemma existify : forall {T}{P : T -> Prop}(x : T), P x -> exists v_0, P v_0.
Proof. (*note that the "v_0" produces the var naming convention in the output*)
  intros T P x H.
  exists x.
  assumption.
Qed.

Inductive Stop_Smuggling_Here := stop_smuggling_here.

Ltac doexistify := 
  match goal with 
      H1:_,H2:_ |- _ => 
      match type of H1 with 
        | Stop_Smuggling_Here => fail 2
        | _ => pattern H1 in H2; apply (existify H1) in H2; revert H1; hnf in H2
      end end.

Ltac smuggler H P :=
  let K:=fresh "K" in
  let E:=fresh "Eq" in
  let H':=fresh H in
  (*generalize_eqs_vars H causes problems - but it would be nice to use here*)
  set (H':=H);
  assert Stop_Smuggling_Here as K by constructor;
  intros;
  assert (JMeq.JMeq H' H) as E by tauto; (*optional, but nice if we can get it to work*)
  revert_until K;
  case H; intros; subst H';
  revert P; repeat doexistify; intros; move E at bottom; clear K;
  match goal with E:?T|-_=>instantiate (1:=T \/ _) in (Value of P) end;
  subst P; tauto.

Lemma or_false_r : forall P, P\/False <-> P.
Proof.
  intros P. tauto.
Qed.

Ltac logicalize H :=
  let P:=fresh "P_" in
  let W:=fresh H in
    revert_until H;
    evar (P:Prop);
    assert P as W by smuggler H P;
    intros;
    (*fill in last evar with False:*)instantiate (1:=False) in (Value of P);
    subst P; 
    (*chop off last False:*)rewrite or_false_r in W.

Section Tests.

  Inductive X : Prop :=
  | X1(Q : Prop) : forall (n: nat)(P:nat -> Prop), P n -> Q -> bool -> forall (m:nat), P m -> n=m -> X
  | X2(Q : Prop) : forall (b:bool)(R:bool-> Prop), R b -> Q -> X
  | X3 : X
  | X4 : 1=2 -> X.

  Variable P : X -> Prop.

  Goal forall x : X, P x -> nat. (*nat induces a non-Prop context*)
  intros x H. logicalize x.
  Abort.

  Inductive Y(n:nat) : nat -> Prop :=
  | Y1(Q : Prop) : forall {P:nat -> Prop}, P n -> Q -> bool -> forall (m:nat), P m -> n=m -> Y n 1
  | Y2(Q : Prop) : forall (b:bool)(R:bool-> Prop), R b -> Q -> Y n 2
  | Y3 : Y n 3
  | Y4 : n=4 -> Y n 4.

  Variable Q : forall m n, Y m n -> Prop.

  Goal forall m n (y : Y (S m) (S n)), Q _ _ y -> nat.
  intros m n y H. logicalize y. (*OK - but is the result usable?*)
  exfalso. (*gets into a Prop context*)
  destruct y0 as [y0|[y0|[y0|y0]]].
  Focus 3.
  (*The JMeqs look OK, but they're not usable!  Why?*)
  Fail rewrite (JMeq.JMeq_eq y0) in H.
  Abort.

End Tests.