coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Top-down proofs in Coq by introducing new variables?

From: Maximilian Wuttke <mwuttke97 AT posteo.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Top-down proofs in Coq by introducing new variables?
Date: Sat, 26 Sep 2020 17:13:16 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mwuttke97 AT posteo.de; spf=Pass smtp.mailfrom=mwuttke97 AT posteo.de; spf=None smtp.helo=postmaster AT mout02.posteo.de
Ironport-phdr: 9a23:OCDtuxPf1WuEyCmn9uIl6mtUPXoX/o7sNwtQ0KIMzox0Iv39rarrMEGX3/hxlliBBdydt6sbzbCM+PC+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oMhm6swrdu8oXjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaktF+grxVoByhpBJxzYDbb46XO/Vica3QZs8aSGlbU8pNSyBMDIOxYo0SBOQBJ+ZYqIz9qkMJoxSkCgisBebvyj5Mhn/3x6I61fkqHgHb3Aw8A9IOs2rbp8jyOacXX+G10bXIzSnAb/xI3Trw6pPFcggmofGXQbJ/b83RxVMyGAzbl1idr5HuMDyJ2OoXqWeb8/ZgWvy1i24hswx9vjqiyMcihITGiY8YxVDJ+yt6zYsrK9O0VVN2bNG6HJVeqi2XKo97TMMsTm9nuCs3y6MLtIKmcCUIyJopyR3SZvqaeIaL+hLuTPudLDR4iX5/eb+yhQy+/Eahx+HmV8S50U5GoylBn9XWq3wA2B3e5tKZRvdj4kutwyuD2g7P5uxCPEs6j7DUK4Q7zb41jpcTsVrMHivxmEjuia+WcVgk+vS05+j5eLnmvpicN5Roig7gNaQigNGwDvogPggPWWiU5/i82aX+8UD6QLhGlPw7n6vDvJ3UJMkXvK+0Dg5N3oYm8Rm/DjOm0NoCnXkAKVJIYBeHjob0O1HSPPD4DumwjlCunTpw3/DGOabhAonTIXjEirvuYKhy51ZGyAUv1dBf+45UCrYZLf3vXU/xrcXUAQM9Mwyp2OnqE85914MbWWKXGKCVKqLSsVmS5uIuOeaAfoEVuCyuY8QisvXplDoynUIXVaivx5oeLn6iTdp8JEDMRHP8g9IAFWYDuEIBUfD2i1DKBTtMemquXK9tuRkjD5m6AICFSo370+/J5zuyApADPjMOMVuLC3q9L9zYCcdJUzqbJ4paqhJBTaKoEtZzzRa1qAL9jbZqfLKNp38o8Kn73d0w3NX90BE/8TstX5aY1HyRFzsyhmQTWzIxmqxy8xQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrUoE9fpRg/GONuEGg+r

On 26/09/2020 16:12, Kumar, Ashish wrote:
> 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.

You could use `edestruct H as [H H']`. This introduces two *existential
variables* ?a and ?b and the hypotheses:

H : P ?a ?b -> Q ?a ?b
H': Q ?a ?b -> P ?a ?b

You will need to `instantiate` the existential variables with some
concrete a and b later. Note that the instantiation is done in the same
proof context as before the `edestruct` tactic.

Another approach is `specialize (H a b) as [H H']` using concrete
instances for a and b right-away.

[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