The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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

Attachment: eq_rel.v
Description: Binary data