The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

I also don't understand why apply is so eager. Try this:

Ltac apply' H1 H2 :=
  let H3 := fresh in (
    (pose proof (H1 H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ _ H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ _ _ H2) as H3; clear H2; pose proof H3 as H2; clear H3) ||
    (pose proof (H1 _ _ _ _ H2) as H3; clear H2; pose proof H3 as H2; clear H3)).

On Mon, Aug 26, 2013 at 6:37 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I guess that was too much for someone to read. So, I'll abstract one of my questions(2nd issue) even further.

All I want is way to request the apply tactic to not attempt to instantiate all the foralls.

In the following example, I want the apply tactic to simply replace (P 1) with (forall m, Q m))

Theorem dont_touch_forall: forall (P Q: nat -> Type),

 (forall n, (P n -> (forall m, Q m)) ) 

  -> (P 1) -> forall m, Q m.

Proof. 

intros ? ?  Hif Hp1. 

apply Hif in Hp1.

Right now. it complains "Error: Unable to find an instance for the variable m."

I know I can finish this proof by first doing intro to get the required m.

But this is the key problem which prevents my rewrite tactic(trw) for typed iff

from working the way Coq's rewrite worked for propositional iff.

(And this is frustrating because just replacing rewrite with trw

isn't enough to revive my old proofs that worked with the propositional iff)

The rewrite tactic for propositional iff does not suffer from this problem of apply.

Require Export Coq.Setoids.Setoid.

Theorem dont_touch_forall: forall (P Q: nat -> Prop),

 (forall n, (P n <-> (forall m, Q m)) ) 

  -> (P 1) -> forall m, Q m.

Proof. 

intros ? ?  Hif Hp1. 

rewrite Hif in Hp1. exact Hp1. 

Qed. 

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Sat, Aug 24, 2013 at 12:00 AM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks. For the moment, we tried to do some more LTac hacking to achieve the desired rewrite functionality. There are still 2 issues that need to be fixed.

Briefly, here is the approach:

In eq_rel.v, build_tiff_term T a b p recursively goes inside prod, sum, implication and t_iff constructors in T and builds a proof object of

T <=> T[b/a], where p is the proof of a<=>b

Ltac build_tiff_term T a b p :=

  match T with

    | a => p

    | ?x -> ?y =>

      let l := build_tiff_term x a b p in

      let r := build_tiff_term y a b p in

      constr:(combine_t_iff_proofs_imp l r)

    | ?x <=> ?y =>

      let l := build_tiff_term x a b p in

      let r := build_tiff_term y a b p in

      constr:(combine_t_iff_proofs_t_iff l r)

    | ?x # ?y =>

      let l := build_tiff_term x a b p in

      let r := build_tiff_term y a b p in

      constr:(combine_t_iff_proofs_prod l r)

    | ?x + ?y =>

      let l := build_tiff_term x a b p in

      let r := build_tiff_term y a b p in

      constr:(combine_t_iff_proofs_sum l r)

    | _ => constr:(t_iff_refl T)

  end.

The trewrite tactics in eq_rel,v are based on this function.

As mentioned before the trouble was that p must be a fully instantiated t_iff relation of the form _ <=> _ . It cannot be something of the form 

forall ....., _ <=> _

We tried to get around this limitation by using the apply tactic to figure out the instantiations. This is implemented in the get_instance_of function below:

Here, the type of T must be of the form:  forall ......, A... <=> B ....

This tactic recursively analyses subterms of H to find a subterm (say t) to which T is applicable in the forward direction

  (i.e something of the form A.... )

It will change the proof state to prove and introduce a lemma of the form (t <=> t') named Hn. (t' is of the form B .....)

Ltac get_instance_of  T  H Hn :=

  match H with

    | _ =>

      assert(Hgetinstanceof:H) by admit;

        progress (apply T in Hgetinstanceof);

        let H2 := type of Hgetinstanceof in

        clear Hgetinstanceof;

          assert (H <=> H2) as Hn by (apply T);

          idtac H

    | ?Hl <=> ?Hr => get_instance_of T Hl Hn || get_instance_of T Hr Hn

    | ?Hl * ?Hr => get_instance_of T Hl Hn || get_instance_of T Hr Hn

    | ?Hl + ?Hr => get_instance_of T Hl Hn || get_instance_of T Hr Hn

    | ?Hl -> ?Hr => get_instance_of T Hl Hn || get_instance_of T Hr Hn

  end.

The trw tactics then pass this fully instantiated lemma to trewrite to do the rewriting.

A sample use of trw is the following:

Theorem trw_demo: forall (P Q: nat -> Type),

 (forall n, P n <=> Q n ) 

  -> ((P 1 * False -> False ) <=> (Q 1 * False -> False )).

Proof. 

intros ? ?  Hiff. trw Hiff .  apply t_iff_refl. 

Qed.

There are still 2 serious problems with this approach.

In the function get_instance_of, I have to use admit to temporarily introduce an arbitrary subterm of H to the context so that

I can try applying the quantified t_iff relation. Although I clear it immediately, I see that the proof object of trw_demo above  has 

a mysterious term trw_demo_admitted2 which has no proof.

---------------

trw_demo = 

fun (P Q : nat -> Type) (Hiff : forall n : nat, P n <=> Q n) =>

(fun Hgetinstanceof : P 1 =>

 (fun H : forall n : nat, P n -> Q n =>

  (fun _ : Q 1 =>

   (fun Hget_instance_of_in_concl : P 1 <=> Q 1 =>

    let Hget_instance_of_in_concl0 :=

      combine_t_iff_proofs_t_iff

        (combine_t_iff_proofs_imp

           (combine_t_iff_proofs_prod Hget_instance_of_in_concl

              (t_iff_refl False)) (t_iff_refl False))

        (combine_t_iff_proofs_imp

           (combine_t_iff_proofs_prod (t_iff_refl (Q 1)) (t_iff_refl False))

           (t_iff_refl False)) in

    let HeqHget_instance_of_in_concl0 := eq_refl in

    (fun

       H0 : (Q 1 # False -> False <=> Q 1 # False -> False) ->

            (P 1 # False -> False <=> Q 1 # False -> False) =>

     H0 (t_iff_refl (Q 1 # False -> False)))

      (let (_, H0) := Hget_instance_of_in_concl0 in H0)) (Hiff 1))

    (H 1 Hgetinstanceof)) (fun n : nat => let (H, _) := Hiff n in H))

  (trw_demo_admitted2 P Q Hiff)

     : forall P Q : nat -> Type,

       (forall n : nat, P n <=> Q n) ->

       (P 1 # False -> False <=> Q 1 # False -> False)

----------------------

The second problem is that this approach does not work if either sides of the t_iff relation begins with a forall.

Probably, the apply  in get_instance_of  fails with "Error: Statement without assumptions"

For example: consider the following

Theorem trw_demo2: forall (P Q: nat -> Type),

 (forall n, P n <=> forall m, Q m ) 

  -> ((P 1 * False -> False ) <=> ((forall m, Q m) * False -> False )).

Proof. 

intros ? ?  Hiff. (trw Hiff || idtac "failed").

Abort. 

Any help in resolving the two issues would be greatly appreciated. The full sourcecode is attached

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Aug 23, 2013 at 2:02 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 23/08/2013 19:58, Abhishek Anand wrote:
> It looks like the setoid mechanism wont work for the t_iff relation because
> it is a relation that lives in Type.

There is an open bug in the bugtracker for this issue:

https://coq.inria.fr/bugs/show_bug.cgi?id=2440

I've been told that it would be fixed by the introduction of universe
polymorphism that should be around by the 8.5 version (already in the
HoTT branch). So, basically, for the moment, be patient.

PMP