coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] weird apply success

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] weird apply success
Date: Tue, 11 Feb 2020 03:23:03 +0000
Accept-language: en-US
Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=IAnnMZJ78wlG11vZsut4hCUKG78zRgNztw8whPyfi7c=; b=kONeEoTxCeGVEOvSUZNKrb7vdD2MkYPnAS+J9fFHeEwVWDdSES+xCk6oA+KUvRHx9WIkzGQbORXHbi+LLaGMRn9j0dVvE5qQDA/ZCLcmZXuHdfry+YMkMzNbdAAYIBlp1oCmdCHDiZRL/B2KtXGJiqMlFd1dc6vL9oVbA1WpzVdLBwIgXDHVvsiG6xH+Rz5GI7B+7BwYL6ZgCDGlL9dORX9EUOsYRq6jpKlRap5mpXhoCk0+PTtawKwfiEpM8Ua0LVlEHgrKZRwNqfWmkgEgMEEkG+RIqsm3ud/Hri56zfniSRME9SeM9NUVi0z4X3cT9ASti8qwbdnszfhq8dgxrg==
Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=NePxjoPWllDrTB/AweyhQHOSzMDwoyMcatM1dDft2S5hiYlbsuWQm2pX7tGBrLcKfY/bV5ROSBc8R92fFCVuxVb4boILftWFHCNOevjHCK+E8ULigo2fP4jH/O+JShF79gny9bynGzdJAMj3A0MZNF+lWgjncc1gnYYMOBSY/JiaR6yB2CiimJ8CV/0ICQns9kaVOh+VLzeoMuPD9Jz4Z/OnancnVLzpe7EePlp9TepvNENl+6RWq9U7yGarRJl69c/fULnbBYyW2OT2/uSEwlB1BiWXDg6oo/UmDweKGs47f7duxFubqJoA52WrTjL++fq/39z1bw9whasjAFQBCw==
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:C1gaJBS0H/byvq7T5PWRrLuVP9psv+yvbD5Q0YIujvd0So/mwa6yYhGN2/xhgRfzUJnB7Loc0qyK6vymBzZLvMjJ8ChbNsAVDFld0YRetjdjKfbNMVf8Iv/uYn5yN+V5f3ghwUuGN1NIEt31fVzYry76xzcTHhLiKVg9fbytScbdgMutyu+95YDYbRlWizqhe7NyKwi9oRnMusUMjoZuN6k8xgHIr3dWdOhbxWJlLk+Xkxrg+8u85pFu/zletv4768JMTaD2dLkkQLJFCzgrL3o779DxuxnZSguP6HocUmEInRdNHgPI8hL0UIrvvyXjruZy1zWUMsPwTbAvRDSt9LxrRwPyiCcGLDE27mfagdFtga1BoRKhoxt/w5PIYIyQKfFzcL/Rcc8cSGFcWMtaSi5PDZ6mb4YXD+QPI/tWr5XzqVUNrBuxGQaiC+z0xz9UnXD7x7E23/g9HQzE2gErAtIAsG7TrNXwLKocVf66zLPWwjXGb/JdxDnz55LGcxA6pvGMW697fM3Vx0YxDQPKkFCQqIz/Mz2bzOsMvXOb7+1mVe+0kWEnrRxxriKxycgxl4nFnJgayk3d+Ch/3Y07JsW4RVZ0bNK4Cpdcqj2WOolsTs8/TWxlujw2xqAItJO/ZCQG1ZQqywLFZ/CZb4SF7AjvWPiMLTtknn5pZbyyihK0/EO90OPzTNO030xPriddktnDqHQN1xvL58WbRPRz41ut1SuW2w7O6O5JL1k4la3AJJE/2LIwkYcTsVjYES/xhUX2irKZel88+uiy7OTnfqvpqYOAN491jQH+NL4imsuiAeQkNggOWG+b+eem2LL/+k35Ra1GjvwwkqbHrJDXPcsWqrKjDwNIzoou6QyzAyqo3dkah3ULMVxIdRafg4jsIV7OIfT4Dfmlg1SrlTdm3/TIMaP7AprTK3jCkK3tc7hn5E9S0wozytZf6olOBbEHPfL/QFH+u8HFDhMjKQO03v7rCM9h2YMGRWKPHqiZPbvOvl+P/+IjOvWDZIsIuDnmMPUl/P7vjXohmVAHZ6Wp3J0XaGq5Hvt8OUmZb2Ds0Z89FjJAtQ0nCefulVeqUDhJZn/0Ubh2rmUwD5vjBoPeTKishqaA1WG1BMsFSHpBDwWuHG3lcpTMd/4TcyWUaptDnyYJUKnnZ4Y+zhaonAb81vxqIveS8zBO5sGr78R8++CGzUJ6zjdzFcnIizjQHVExpXsBQnoN5I46oUF5zQvcg4FFuKQBUOdivLZOWAp8MoPAxetnDdy0QhjGYtqCVFehRJOhHC01SdUyhdQJZhQkQonwvlX4xyOvRoQtufmTHpVtqPDV2WW3KspgjX/bhvF43gsWB/BXPGjjvZZRsg3aBorHiUKczvz4fKIBmiPB6SGK0DjXsQ==

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