The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a good way to take

  f : a -> T a a -> Prop

and turn it into

  g : a -> b -> T a b -> Prop

so that we can prove

  f _ x <-> g _ _ x

and

  b <> a -> ~g a b _

?

Essentially, I want to take [T a a -> Prop] and generalize it to [T a b -> Prop] such that I don't get any new truths that I didn't already have from my original function.

I was able to write the following code which does what I want, but I'm wondering if there's a better/simpler way to do it, and if there's a way to write [cast] so that I don't need [eq_rect_eq] to prove [cast_nop]:

Require Import Eqdep.

Import Eq_rect_eq.

Set Implicit Arguments.

Parameter f : forall T (a : Type), T a -> Prop.

Implicit Arguments f [T a].

Inductive and' (A : Prop) (B : A -> Prop) : Prop :=

  conj' : forall (a : A), (B a) -> @and' A B.

Implicit Arguments and' [].

Definition cast T (a b : Type) : a = b -> T a b -> T a a.

  intro H. rewrite <- H. intro t. apply t.

Defined.

Definition g T (a : Type) (b : Type) (x : T a b) : Prop :=

  and' (a = b) (fun p => f (cast T p x)).

Implicit Arguments g [T a b].

Theorem g_ne T (a b : Type) (x : T a b) : a <> b -> ~g x.

  unfold g; firstorder.

Qed.

Lemma cast_nop T (a : Type) (x : T a a) (p : a = a) : x = cast _ p x.

  unfold cast; rewrite <- eq_rect_eq; reflexivity.

Qed.

Hint Resolve cast_nop.

Theorem f_eq_g T (a : Type) (x : T a a) : f x <-> g x.

  unfold g; firstorder;

    try (

      match goal with

        [ |- (and' (?a = ?a) _) ] => cut (a = a); try solve [ reflexivity ]

      end; 

      intro p; apply (@conj' _ _ p)

    );

    match goal with

      [ H : f ?arg1 |- f ?arg2 ] => cut (arg1 = arg2); eauto

    end;

    intro h; rewrite <- h; assumption.

Qed.

Thanks!

-Jason