The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Jason,

How about something using the same kind of construction
as the identity type?


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

Implicit Arguments f [T a].

Inductive g T (a : Type) : forall (b : Type) (x : T a b), Prop :=
  | injf : forall (t : T a a), f t -> g T a a t.

Implicit Arguments g [T a b].

Theorem g_ne T (a b : Type) (x : T a b) : a <> b -> ~g x.
  intros H gx ; inversion gx ; contradiction.
Qed.

Theorem f_eq_g T (a : Type) (x : T a a) : f x <-> g x.
split.
 intro fx ; constructor ; assumption.
 intros [] ; firstorder.
Qed.


Cheers,

--
gallais


On 28 May 2012 21:34, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> 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
>