coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Cyprien Mangin <cyprien.mangin AT m4x.org>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] subst surprise
- Date: Thu, 26 May 2016 05:18:51 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=Neutral smtp.pra=cyprien.mangin AT m4x.org; spf=Pass smtp.mailfrom=SRS0=w3aN=RT=m4x.org=cyprien.mangin AT bounces.m4x.org; spf=Pass smtp.helo=postmaster AT mx1.polytechnique.org
- Ironport-phdr: 9a23:BMbKgxy69493dBTXCy+O+j09IxM/srCxBDY+r6Qd0e4WIJqq85mqBkHD//Il1AaPBtWKra4YwLWN+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuSt+U05j8iLv60qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mosVHSODxe7kyZb1eFjUvdW4vt+PxshyWZhqX/HoRVC0zmxxHAg6NuBrrRo3wvy28s+N71yicFciqXfYzQzv0vPQjcwPhlCpSb21xy2rQkMEl1K8=
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
- [Coq-Club] subst surprise, Jonathan Leivent, 05/26/2016
- Re: [Coq-Club] subst surprise, Cyprien Mangin, 05/26/2016
Archive powered by MHonArc 2.6.18.