coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Kumar, Ashish" <azk640 AT psu.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: [Coq-Club] Top-down proofs in Coq by introducing new variables?
- Date: Sat, 26 Sep 2020 14:12:54 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=psu.edu; dmarc=pass action=none header.from=psu.edu; dkim=pass header.d=psu.edu; 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=J97+urkvfZ+zJ27vk42kvJpaAiyd9LJ6JR/An7iY2AI=; b=Dv354HeOYK4gFrsCtPmgm1Nkmd/lpYFXbzfo9BmjYAn7HZKxnIb+BQY/ZIyMi0jzHHP+EeeTK7r6DvejG+Ss6+ApPi9Ha54fud3drc2kWTcOPiY26FGDUubAosgL54PB4r5kP1UiRyVPv2XZBiVIu5ycogH2/sT1Y1GGPKtKWSB3okWf0imqlAJfquFncIdVgrao4m/z+o6UfqdyRGj+Wb2/24NUxNVPARpOziab1wQL7+MIxknrVkHdhrHur+3SBUPKuq+scjTLubU7lbB3ZKhix/FYPmOKg9nedmTmEqMslP/XOi6pkxW7zhtnWCoentstXrPRreaWgAnc9jwdEw==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=nHWg/gtb8bPNt2GVgnWUlQy+N+sMp+n1WrYeFKZRGGEsH5i9jCa5TwZ6H+RV1XsxO5PbrTu4cj1PotVYnvfI65NgumAlMqAGgUQ37fmJ/fgjfhClJfTZd5sDwNbxKt+qMRpAJYPULSarKJxrW2IxBlB5G0dQkGq6ac8nZGT+2kILTDRVyTNShnSiJEmoWUUB4VKZmTHiR/p1rAuE91MA1+bjJ6EgJ5IdvOFm8SLtCcBzEm68+2e8L1mgu8KRoDLXdQBd3H35YV4J2nSzsfu39SxIwe4qTRPeFp7K0xMXFGK0WVLgxWw5+1mArCcZ7zr0ggRCZLT0P5lu6FfCmTWQ1w==
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=azk640 AT psu.edu; spf=Pass smtp.mailfrom=azk640 AT psu.edu; spf=Pass smtp.helo=postmaster AT NAM12-BN8-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:NA8+UxcWZajasd+H6hpkEVhalGMj4u6mDksu8pMizoh2WeGdxcW6Yx7h7PlgxGXEQZ/co6odzbaP7Oa6Aydfvd6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLhi6txvdutcZjYZgJas61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9Zwgbpbrhy/uhJ/34DaboKUNPVicazQZskVSXZdUstLSyBNHp6wYo0SBOQBJ+ZYqIz9qkMAoRW7GAmsAfngyiVQinTrwaA6yOQhEQDd3AwgEd4FrXPZo8/0NacRUO24w7XEwC7bb/NNxDfx8pbHfQ08ofyVW797bMXex1U1GQzfklWQtZLqPymT1ukVs2aW7+ptWOaxh2MmqAx9vDehy8UjhIfGiYwY11HJ+CF2zYorONC1VU92bNCmHZdMuS+UOYV7T8A/T212pis217sLsoO4cigS0JkqyALTZ+aaf4SU4B/vTvidLDl6iX5/Zb6yiRS//VC9xuHgWcS4ylhHoylfntTDqHwBzR3e5tWfRvdj/0qtxTiC2gXO5u1YOk85lK/WJIQ9zrM+k5cevlrMEyrzlUnrkKObcFgv9PKy5OT9eLrmo4eRN49qhQH6NaQjgtSxDPg/PAQTQWSX4Pmx2qXg8EHgR7VFleM5nrPesJDHOcQUvam5AxJT0ok+8Rq/Fy2m0NMEnXYZMF1FZBOHj4/vO13UJ/D4EOu/g1CrkDdsxPDKJKHuApLILnTbkbfhe6hy61JExQc80dxT/Y9YBq0DLf7pREP8ut7VAgUkPwG6wevrENB92ZkfWWKLDK+ZKqTSsVqQ6+01IuiMZ44YtTnhJ/U+//7ulmI5lUUDcqa0wJsbcGq4Eeh+I0WFfXrshc8MHnsNvgonVeDllFmCUSNIaHupRKI95jQ7CJq8AovZR4CthqaB3CahEZFMaGBGEAPELXC9PY6DQrIHbD+YCs5niD0NE7a7Acd13ha38QT+1rBPL+zO+yReu4i1h/Zv4OiG3zIv8DVuS4y0yGGMVGE+1jcBVTxogPhXuVdgjFqPzP4r0LRjCdVP6qYRAU8BPpnGwrkiUoGgakf6Zt6MDW2ebJCjCDA1QMg2xo5ce11gXdiuk0Kahnb4M/ouj7WOQacM3OfExXGgdd5m1jDL2LRz1wB7EPsKDnWvg+tEzyaWB4PNlBnGxYCDUP1GmQTrpCKEx2fIu1xEWgltV6mDRWoYekbdsdX+4AXFUqOqDrMkdABGzJzbJw==
In a particular proof I was working on, I had the following hypothesis and goal:
H: forall a b, P <-> Q.
------------------
False
Context: a and b are user defined inductive types, and P and Q are propositions which use a and b.
Idea on how to prove it: Informally, the above proof holds as (for all a b, ~Q ) holds and I can supply some specific value of a and b, for which P holds.
So using the above idea, I proved the result, using a bottom-up approach i.e. by proving the following intermediate results using 'assert'.
Proof.
assert{H1: forall a b, ~Q}. { ... }
assert{H2: P' }. { ... } (* P' is an instance of P with specific a and b values.*)
assert(H3: ~(P' -> Q') ). { ... }
assert(H4: ~(P' <-> Q') ). {... }
unfold not in H4, apply H4; apply H. Qed.
My question is that is there some way I could have use 'destruct' on the original H, to produce variables a0, b0 and hypothesis H1: P -> Q and H2 : Q -> P, i.e. a top-down approach? If so, I could have gotten a contradiction very easily by H1 and H2. I can't use it now, as I don't have any variables in proof context to supply a and b with.
With regards,
Ashish
H: forall a b, P <-> Q.
------------------
False
Context: a and b are user defined inductive types, and P and Q are propositions which use a and b.
Idea on how to prove it: Informally, the above proof holds as (for all a b, ~Q ) holds and I can supply some specific value of a and b, for which P holds.
So using the above idea, I proved the result, using a bottom-up approach i.e. by proving the following intermediate results using 'assert'.
Proof.
assert{H1: forall a b, ~Q}. { ... }
assert{H2: P' }. { ... } (* P' is an instance of P with specific a and b values.*)
assert(H3: ~(P' -> Q') ). { ... }
assert(H4: ~(P' <-> Q') ). {... }
unfold not in H4, apply H4; apply H. Qed.
My question is that is there some way I could have use 'destruct' on the original H, to produce variables a0, b0 and hypothesis H1: P -> Q and H2 : Q -> P, i.e. a top-down approach? If so, I could have gotten a contradiction very easily by H1 and H2. I can't use it now, as I don't have any variables in proof context to supply a and b with.
With regards,
Ashish
- [Coq-Club] Top-down proofs in Coq by introducing new variables?, Kumar, Ashish, 09/26/2020
- Re: [Coq-Club] Top-down proofs in Coq by introducing new variables?, Beta Ziliani, 09/26/2020
- Re: [Coq-Club] Top-down proofs in Coq by introducing new variables?, Maximilian Wuttke, 09/26/2020
- Re: [Coq-Club] Top-down proofs in Coq by introducing new variables?, jonikelee AT gmail.com, 09/26/2020
Archive powered by MHonArc 2.6.19+.