Destructing term when match generates equality involving that term

Using Coq
1

Hello everyone,
recently I have run into problems with dependencies preventing me from destructing terms I match on when the branches of the match use the equality generated by the match.
For example I have something like the following scenario:
I have types function and type as well as functions get_type and has_type that infer a type for a function (if possible) and check that a function has a given type.
I also have a lemma get_type_correct that relates get_type and has_type.

Hypothesis function: Type.
Hypothesis type: Type.
Hypothesis get_type: function -> option type.
Hypothesis has_type: function -> type -> Prop.
Hypothesis get_type_correct: forall f t, get_type f = Some t -> has_type f t.

I have then defined an inductive type typed_function that packages a function together with its type and a proof that the type is correct. I have also defined two functions converting between typed and untyped functions.

Inductive typed_function : Type :=
  TR f t:  has_type f t -> typed_function.
Definition untype_function (tf: typed_function):=
  match tf with
  | TR f _ _ => f
  end.

Definition type_function (f: function) : option typed_function.
  destruct (get_type f) eqn:E.
  - exact (Some (TR _ _ (get_type_correct _ _ E))).
  - exact None.
Defined.

Note that type_function needs the equation E generated by the case analysis of (get_type f) to construct the proof needed by the TR constructor.
The actual definition generated by Coq from my tactics is the following:

type_function =
fun f : function =>
let o := get_type f in
let E : get_type f = o := eq_refl in
match o as o0 return (get_type f = o0 -> option typed_function) with
| Some a => (fun (t : type) (E0 : get_type f = Some t) => Some (TR f t (get_type_correct f t E0))) a
| None => fun _ : get_type f = None => None
end E
     : function -> option typed_function

I would like to prove that removing the types from a term that has been successfully typed via type_function results in the original term. However, as far as I can tell, this would require me to do case analysis on get_type f, which Coq will not let me do because it results in wrong types in the return branches.

Lemma untype_of_type_eq f tf: type_function f = Some tf -> untype_function tf = f.
Proof.
  unfold type_function. intros eq.
  Fail destruct (get_type f).

The command has indeed failed with message:
Abstracting over the term “o” leads to a term
fun o0 : option type =>
match o0 as o1 return (o0 = o1 → option typed_function) with
| Some a => fun E : o0 = Some a => Some (TR f a (get_type_correct f a E))
| None => fun _ : o0 = None => None
end eq_refl = Some tf → untype_function tf = f
which is ill-typed.
Reason is: Illegal application:
The term “get_type_correct” of type
“forall (f : function) (t : type), get_type f = Some t → has_type f t”
cannot be applied to the terms
“f” : “function”
“a” : “type”
“E” : “o0 = Some a”
The 3rd term has type “o0 = Some a” which should be coercible to “get_type f = Some a”.

Even dependent destruction does not work:

  pose (gf := get_type f). fold gf in eq.
  Fail dependent destruction gf.

The command has indeed failed with message:
gf is used in hypothesis eq.

I have not been able to figure out how to deal with such situations and would be very happy about any help.

Cheers,
Jan.

2

Here’s an approach that works, following the motto of embracing the computational behavior of equality proofs:

(* eq_trans matches on H0, which does not work in our case, we must match on H. *)
Definition eq_trans2 {A} {x y z : A} (H : y = x) (H0 : y = z) : x = z :=
match H in (_ = a) return (a = z) with
| eq_refl => H0
end.

Lemma untype_of_type_eq f tf: type_function f = Some tf -> untype_function tf = f.
Proof.
  unfold type_function.
  assert (forall (oe : option type) (He : oe = get_type f),
        match oe as o return (oe = o -> option typed_function) with
    | Some t =>
        (* Combine the equality proofs *)
        fun E : oe = Some t => Some (TR f t (get_type_correct f t (eq_trans2 He E)))
    | None => fun _ : oe = None => None
    end eq_refl = Some tf -> untype_function tf = f) as H.
  - intros oe He. destruct oe.
    + simpl. destruct tf. simpl. intros [= -> ->]. easy.
    + intros [=].
  - specialize (H _ eq_refl). simpl in H. eapply H.
Qed.
1 Like
3

The issue with destruct (get_type f) is that Coq tries to generalize all the occurrences of get_type f before destructing it. Unfortunately, with the kind of term you are manipulating, this is usually a poor strategy, as it leads to ill-typed terms. So, you have to generalize the sub-terms manually:

Lemma untype_of_type_eq f tf: type_function f = Some tf -> untype_function tf = f.
Proof.
unfold type_function.
generalize (eq_refl (get_type f)).
generalize (get_type f) at 2 3.
now intros [t|] E [= <-].
Qed.

In particular, try to understand why eq_refl had to be generalized before get_type f.

2 Likes
4

Oh, very nice. I never even thought about generalizing eq_refl. This seems to generate a version of the assert from the previous solution without having to write it down manually and without the need for eq_trans2.
Figuring out exactly which occurrences of (get_type f) need to be generalized seems to be quite tricky though.

5

Here it is quite simple and purely syntactic. The goal looks as follows (with g denoting get_type f):

forall e: g = g, match g as o return (g = o -> ...) with ... end e = ... -> ...

First, you need to generalize the occurrence of g that is being matched upon (that is the reason for calling destruct in the first place). Since e is of type g = g while the return clause expects g = o, you also need to generalize the right-hand side of g = g. That is it.

1 Like
6

By the way, this also explains why it was important to generalize eq_refl g first. Otherwise, you would need to generalize this occurrence of g to please the right-hand side of the return clause, but also not to generalize it to please the left-hand side of the return clause. Obviously, it is impossible to do both. So, by generalizing eq_refl g, we get e: g = g, and now we can handle both occurrences of g differently.