coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there a tactic to do this in a convenient way?

From: Gabriel Scherer <gabriel.scherer AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Is there a tactic to do this in a convenient way?
Date: Sat, 12 Nov 2016 13:06:43 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f68.google.com
Ironport-phdr: 9a23:swKUuRWASzrJ86OjzpbhnZv1f+LV8LGtZVwlr6E/grcLSJyIuqrYYxyOt8tkgFKBZ4jH8fUM07OQ6PG7HzRfqs/Y6DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal8IRiyowjdrNUajIltJqos1xfFvmZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zMlMd+kLxUrw6gpxxnwo7bfoeVNOZlfqjAed8WXHdNUtpNWyBEBI63cokBAPcbPetArYb9qVsAoxW9CwexGu3g1iRFiWXq0aAgyektDR3K0Q4mEtkTsHrUttL1NKIKXO601qbH1i/Db/JI1jf59YPGbwwuofGSUrJqb8XR01QkGgTKjlqKsoPlJTKV2foJs2SB9OpvSeKvhHA9qw5vuDii3cgsiozTiYIUzlDI7zl2wIEwJdChTkNwfN2qEINIui2EK4d7RtkuTmJotSog1LEKpJG2cDILxZkkwRPUduaJfJKS4h35UeacOTd4i2xheLK4nxuy9FKvyuz4VsWt0VZKsjZJnsDCtn0M1BHf8MeHSvx6/keu3TaAyRrf5f1DIUAxjabbKpghzaAslpcLr0jPAiv7lF/1gaKWbEko5PWk5uv9brjnpZKQL4p0hRv/MqQqlMy/G+M4Mg0WUmiU4+uzz6fj/UznT7VOlPE2ibXWsJDEKsQBuKG5GRRY0okm6xmlDjem1M4UkmUALFJAYB6HlZTmO0nSIPDkCveym0ijkDByx/zfIrLhBojNIWPYnbf6fbd97lZcxxApwdBe4ZJUELABL+jpVk//rtyLRiM+Ziez2q7MDMh3ntcVXnvKCauEOovTt0WJ76QhOb/fSpUSvWPSIvI/5vPqxUQymVIHcLPhiZQeYmq5E/AgOE6ZbGDhmP8OFG4Lukw1S+m82w7KaiJae3vnB/F03To8Eo/zSN6bHo0=

Indeed, refine is very elegant here. Reformulated in my previous presentation, it gives:

Parameters LongA LongB LongC LongD : Type.

Parameter long_term : LongA -> LongB -> LongC.

Goal LongD.
Proof.
refine (_ (long_term _ _)); [intro H | | ].
(* three subgoals:
     H:LongC |- LongD
     |- LongA
     |- LongB
   *)
Admitted.

On Sat, Nov 12, 2016 at 12:27 PM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:

On 11/12/2016 04:42 PM, Chris Dams wrote:

Dear all,

In a proof I have a long and complicated term (let us call it
long_and_complicated_term) that is of a type that is of the form A -> B
-> C where all of A, B, and C are also long and complicated.

with the standard tactic:

Goal forall A B C D, (A -> B -> C) -> D.
intros A B C D H.
refine (_ (H _ _)); try intro H1.

--
Laurent

[Coq-Club] Is there a tactic to do this in a convenient way?, Chris Dams, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Xavier Leroy, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Jonathan Leivent, 11/12/2016
  - Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Jonathan Leivent, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Gabriel Scherer, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Dominique Larchey-Wendling, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Laurent Thery, 11/12/2016
  - Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Gabriel Scherer, 11/12/2016
  - Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Chris Dams, 11/13/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Gaetan Gilbert, 11/12/2016