Removing trivial match clause in Coq

user_1598568 0
Viewed 152

Consider the following example:

Definition cast {A : Set} (B : Set) (prf : A = B) (x : A)   : B.
  rewrite prf in x.
  refine x.
Defined.

Lemma castLemma0 {A : Set} : forall (x : A) prf, cast A prf x = x.
Proof.
  intros.
  compute.
???

After the compute step, we are left with the following context and subgoal

A : Set
x : A
prf : A = A
______________________________________(1/1)
match prf in (_ = y) return y with
| eq_refl => x
end = x

Clearly the left hand side and right hand side are equal. But I am not sure how to get rid of the annoying 'match' clause on the left hand side. In particular, trying to destruct prf yields the following error

Abstracting over the terms "A" and "prf"
leads to a term
fun (A0 : Set) (prf0 : A0 = A0) =>
match prf0 in (_ = y) return y with
| eq_refl => x
end = x which is ill-typed.
Reason is: In pattern-matching on term 
"prf0" the branch for constructor 
"eq_refl" has type "A" which should be 
"A0".

Is there a way to get rid of this match clause?

coq pattern-matching
2 Answers

This is not provable in Coq without assuming an extra axiom, usually eq_rect_eq or something equivalent (Uniqueness of Identity Proofs (UIP) or Axiom K).

If you restrict castLemma0 to the eq_refl case, that is forall (x : A), cast A eq_refl x = x, this is provable by reflexivity.

One way to understand why this is not provable, is to accept that it is consistant to assume an axiom bool_eq_not : bool = bool such that cast bool bool_eq_not x = not x. Plugging in bool_eq_not for prf in castLemma0 would imply that not x = x, which is certainly wrong.

Proving that this is possible requires demonstrating a model of type theory where bool_eq_nat is constructible. This was first done in the paper "The groupoid interpretation of type theory", by Martin Hofmann and Thomas Streicher. There have since been several other models, including a model in simplicial sets by Voevodsky, and several constructive models in cubical sets. These investigations are one aspect of the field of Homotopy Type Theory (HoTT).

As a side note, there is a somewhat recently added (and still experimental) feature SProp (documentation) that if you also Set Definitional UIP lets you prove this.

user_26443680

Because prf is an identifier, the dependent destruction tactic (from Coq.Program.Equality) can handle the dependency on prf0 introduced by the convoy pattern. For example:

Require Import Coq.Program.Equality.

Lemma castLemma0 {A : Set} : forall (x : A) prf, cast prf x = x.
Proof.
  intros.
  compute.
  dependent destruction prf.
  reflexivity.
Qed.

(I don't know if dependent destruction relies on any new axioms under-the-hood, though—maybe someone else can help clarify.) UPDATE: OP found that it uses eq_rect_eq (≣ injectivity of dependent equality ≣ uniquness of identity proofs ≣ uniqueness of reflexive identity proofs ≣ axiom K, according to Coq.Logic.EqdepFacts). Unfortunately, that makes this particular proof rather circular. Still, I'll leave this answer up in case others find it useful.

It's also worth noting that if you wanted to dependently destruct an expression, rather than just an identifier, that tactic and its relatives don't work anymore. I don't actually know the solution to this, or even if there is one in general. (For a more thorough discussion with those much more knowledgeable than me, see https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/.60dependent.20destruction.60.20of.20expressions/near/209916250.)

user_23912440
Related