The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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