coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] weird apply success

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] weird apply success
Date: Mon, 10 Feb 2020 22:37:04 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f54.google.com
Ironport-phdr: 9a23:Cc4NHB88HHjeaP9uRHKM819IXTAuvvDOBiVQ1KB41uscTK2v8tzYMVDF4r011RmVBNmdtagP1rue8/i5HzBZutDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMXjId8Jao8yh/EqWZMd+hK2G9kP12ekwvy68uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjeK7WYNEUSndbXstJWCNBDIGzYYsBAeQCIOhWsZXyqkAUoheiHwShHv/jxiNKi3LwwKY00/4hEQbD3AE4G9wBqm/UrNLzNKwPUO611q7IzS7Yb/hL3jr96pLHcgsmofGKUrJwa83RyVI0Fw7BlViQponlMCmU1uQJqWSU8+1gVee2hmMhtgp/oSCvy98yhoXVgo8Z0FPJ+CVjzIorOdG1S1R3bN6rHZZWqiqULZF5Qtk4TGFtoCs6yqMJuZq8fCUSzZQo3R/fa/ief4eW/x3vSf+dITl4iX9qYr6/iBGy8U+vyu34SMa4ykpFri1AktXUt3AN0QLc6tSfR/dj4kus3SyD2gPT5+1eP0w4ianWJ4Qhz7M/jpYTtF7MHi7ymEX4lq+WcUAk9/Cq6+v9ebXmoZmcN4BuigH5KaQugciyDP83MggLRWeb+OC82Kf/8k3+RbVGluc2nbXBsJDGOcQboba0DBNS0oY68hqwEzOm0MkDknQcN1JEeBeHj5DzNF3UIfD4C+2/g1W2nztxyfDGJO6pPpKYJX/a1bzlYLw1v0Vb0U84yc1Vz5NSELAIZvzpDBzfrtvdWz0wKAuyi8n9D85mntccUHmIBKCDN7jJ4HeH4+suJ6+HY4pD62W1EOQs+/O71SxxolQaZ6T8hcJLOkD9JexvJgCiWVSpms0ISD5YsQ83Teisg1qHA2YKOiSCGpkk7zR+M7qISIfOQof33e6E1Sa/W5BaPyVIVwzKHnDveIGJHfwLbXDKe54zonk/TbGkDrQZ+1SrvQ7+xaBgK7ONqCIdvJPnktNy4r+KmA==

The apply tactic executes some reduction. If you run simpl or cbn on your goal, you should see a closer match to the conclusion of your lemma.

On Mon, Feb 10, 2020, 22:23 Jeremy Dawson <Jeremy.Dawson AT anu.edu.au> wrote:

Hi,

I have a goal

seqrel (sctr_relR (Var pp)) ([], (([Var pp] ++ H2) ++ l0) ++ [Var pp])
([], ([Var pp] ++ H2) ++ l0)

and a lemma

can_trf_sctrR_pp < Check sqr_sctr_relRI.
sqr_sctr_relRI
: forall (V : Type) (fml : V) (S : list V),
seqrel (sctr_relR fml) ([], fml :: S ++ [fml]) ([], fml :: S)

I (accidentally) entered the command
apply sqr_sctr_relRI.

and it seemed to solve the goal, which it clearly shouldn't

What is happening here?

Thanks

Jeremy

[Coq-Club] weird apply success, Jeremy Dawson, 02/11/2020
- Re: [Coq-Club] weird apply success, Jason Gross, 02/11/2020