coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] clone evars in destruct

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] clone evars in destruct
Date: Fri, 15 Jan 2021 13:18:37 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-io1-f51.google.com
Ironport-phdr: 9a23:4qpHth0jv5giSEi/smDT+DRfVm0co7zxezQtwd8ZseMTKfad9pjvdHbS+e9qxAeQG9mCurQc0aGP6fioGTRZp8rY7zZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq80bjZF+JqovxRfFv2VEd/hLzm9sOV6fggzw68it8JNh6Shcp+4t+8tdWqjmYqo0SqBVAi47OG4v/s3rshfDTQqL5nQCV2gdjwRFDQvY4hzkR5n9qiT1uPZz1ymcJs32UKs7WS++4KdxSR/nkzkIOjgk+2zKkMNwjaZboBW8pxxjxoPffY+YOOZicq7bYNgXQ3dKUMRMWCxbGo6zYIsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4Et8Sq3vUrNT1NLwSUe+rz6nD0CnOb/VM1jf79YfDbxcsruuXUrJwcMrR0kkvGB3GjlmKs4PlOSma1uIQvGSB7upgVP6vi2E8pgF+pzig3MYsio3Tio0JzVDE8Dx0zYAoLtK3VEB1e8SrEIdMty6ELYt2RNsvTmF2tCg0xbMLupG1cSsKxponyBDSZPOKfouV7x7+VeucJSl1iW5qdb+8hRu8/lStx+7hW8S0zFtHrSpLn9vRun0Lyhfd5M+HSv5n8Ueg3zaCzxzc6uZeIUAyi6XbL5ohzqQumZUOrETPBjP5mELsjK+QaEok/uyo5/79brr4u5CcKol5gRz9PKQ2gsGzH/g0PwwUU2WY+emwzqDv8Ez4TblQjvA6j6/Uu43AK8sBvK62GQpV354j6xmhCzem18wVnXwdI1JEfBKLlonpO1bTLPzhA/eyg0mgnC1kx/DBOb3hDZHNIWbZnLj9erZ97lZQyAs1zd9B+5JZEq8NLO73V0Prt9HVDgU1PxG1zuvmEtlw1p4SVXqKAqCDMaPStVGI5vgoI+mJfIIaoi3yK/gk5/71jX82h1wdcbOz0psRcn+4GOlpL1+YYXrtntcBHnwHvgU7TOPwiV2CVSRfaGq1X6I5/j07Ep6pDZ/fRoCxh7yMxDu0HppPZmxfFl+MFWroeJ6fVvcXaCOSJ9dhnSYeWbigTY8hzxCuuxXgx7ppNOqHshEf4JnkzZ1+4/DZ3UU58iUxBMCA2UmMSXt1lyUGXWll8rp4pBlUwFeCyqh1gLRxE9VV67sdWw06NIXcwu88Atb7XA6Hf9aVR36pR9ynBXc6SddnkIxGWFp0B9j31kOL5CGtGbJAz+XXVqxxybrV2j3KH+g402zPjfBzgFwvQ88JPmqj1PYmplrjQrXRmkDcrJ6EMKEV3SrD7mCGlDPcs0RRUQo2WqLADylGOxnm6O/h70aHdIeATLQqNgwblJyHI6pOL9zu1BBIGa6lN9PZbGa83Wy3AETQyw==

eexists is very helpful in proofs because it lets us avoid computing/simplifying complex things in our head and let Coq do all that and almost figure out the right answer.

However, the eexists implementation in Coq does not achieve the full potential.

For example, making cases is dangerous as it requires the value on both sides to be equal:

Require Import Nat.

Lemma xx (b:bool): exists n, n = if b then 1 else 2.
eexists.
destruct b.
- reflexivity.

- (* cant prove 1=2 *)

Abort.

In the above simple/contrived, the right answer is immediately clear but it is not the case in many proofs. Is there a way to ask destruct to clone some chosen evars for each case as I did below manually:

Lemma xxx (b:bool): exists n, n = if b then 1 else 2.
eexists.
Unshelve.
Focus 2.
evar (x:nat).
evar (y:nat).
exact (if b then ?x else ?y).
simpl.
destruct b.
- reflexivity.
- reflexivity.
Qed.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

[Coq-Club] clone evars in destruct, Abhishek Anand, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Hugo Herbelin, 01/15/2021
  - Re: [Coq-Club] clone evars in destruct, jonikelee AT gmail.com, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Clément Pit-Claudel, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Siegfried, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Maximilian Wuttke, 01/15/2021
- Re: [Coq-Club] clone evars in destruct, Jeremy Dawson, 01/16/2021