The Coq mailing list

[Cyprien Mangin <cyprien.mangin AT m4x.org>]

Since you are rewriting a to b (and not the other way around), you have to match on eq_sym x in some way, hence the multiple matches.

So subst b would give a very simple term.

Note that if you do it with a rewrite <- x in *; clear x (and have the goal depend on x, so that it does not just discard it), the proof term is actually very similar.

On Thu, May 26, 2016 at 5:06 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

I thought that the subst tactic just did some rewrites followed by clears.  Not quite:

Variable P : forall {a b:unit}, a = b -> Prop.
Lemma foolish(a b : unit)(x : a = b)(p : P x) : True.
Proof.
  subst a.
  exact I.
Defined.
Definition wtf := Eval cbv in foolish.
Print wtf.

prints (in 8.5pl1):

wtf =
fun (a b : unit) (x : a = b) (p : P x) =>
match
  match
    x as H in (_ = y)
    return
      (match match H in (_ = y0) return (y0 = a) with
             | eq_refl => eq_refl
             end in (_ = y0) return (y0 = y) with
       | eq_refl => eq_refl
       end = H)
  with
  | eq_refl => eq_refl
  end in (_ = H) return (P H -> True)
with
| eq_refl =>
    match
      match x in (_ = y) return (y = a) with
      | eq_refl => eq_refl
      end as H in (_ = y) return (P match H in (_ = y0) return (y0 = b) with
                                    | eq_refl => eq_refl
                                    end -> True)
    with
    | eq_refl => fun _ : P eq_refl => I
    end
end p
     : forall (a b : unit) (x : a = b), P x -> True

Does anyone know what's going on here?

-- Jonathan