The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

David Singh wrote:
>   This can be defined as follows:
>
>    Require Import Program.Equality.
>
>     Definition pPT n I (t : T PT n) (x : EPT (P3 n) (cn I t)) : PPT x.
>     intros n I t x; dependent destruction x. exact (pp3 _ ).
>    Defined.
>
>   This is fine until one has to prove things involving pPT; the function
>    reduces to a large, complicated expression. I was wondering if 
> there is a
>    better way to define pPT *without* the use of dependent 
> destruction, and which
>   would reduce as it should?

"Better" is in the eye of the beholder, but here's an axiom-free version 
that reduces naturally.  This was a bit of a puzzle to figure out, but I 
find the solution reasonably simple/modular, as these things go.


Definition Thead F n (t : T F (S n)) : F n :=
  match t in T _ n' return match n' with
                             | O => unit
                             | S n'' => F n''
                           end with
    | e => tt
    | cn _ x _ => x
  end.

Definition Ttail F n (t : T F (S n)) : T F n :=
  match t in T _ n' return match n' with
                             | O => unit
                             | S n'' => T F n''
                           end with
    | e => tt
    | cn _ _ y => y
  end.

Lemma decomp' : forall F n (t : T F n),
  match n return T F n -> Prop with
    | O => fun _ => True
    | S n' => fun t => t = cn (Thead t) (Ttail t)
  end t.
  destruct t; trivial.
Defined.

Theorem decomp : forall F n (t : T F (S n)),
  t = cn (Thead t) (Ttail t).
  intros; exact (decomp' t).
Defined.

Definition p3inv n (pt : PT n) (t : T PT n) (x : EPT pt t) :=
  match x in EPT pt t
    return match pt in PT n return T PT n -> Type with
             | P3 _ => fun t => EPT (Thead t) (Ttail t)
             | _ => fun _ => unit
           end t with
    | p3 _ _ _ x' => x'
    | _ => tt
  end.

Lemma p3inv_same' : forall n (pt : PT n) t (x : EPT pt t),
  match pt return forall t, EPT pt t -> Prop with
    | P3 _ => fun _ x => p3 (p3inv x) = match decomp _ in _ = T return 
EPT _ T with
                                          | refl_equal => x
                                        end
    | _ => fun _ _ => True
  end _ x.
  destruct x; trivial.
Defined.

Theorem p3inv_same : forall n (I : PT n) t (x : EPT (P3 n) (cn I t)),
  p3 (p3inv x) = x.
  intros; exact (p3inv_same' x).
Defined.

Definition pPT n I (t : T PT n) (x : EPT (P3 n) (cn I t)) : PPT x :=
  match p3inv_same x in _ = T return PPT T with
    | refl_equal => pp3 (p3inv x)
  end.

Theorem pPT_red : forall n (t : PT n) (ts : T PT n) (x : EPT t ts),
  pPT (p3 x) = pp3 x.
  reflexivity.
Qed.