Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] subst surprise

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] subst surprise


Chronological Thread 
  • 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=

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






Archive powered by MHonArc 2.6.18.

Top of Page