coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Maxime Dénès <mail AT maximedenes.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] simpl should reduce on constructor?
- Date: Sat, 29 Oct 2016 20:44:25 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 8.mo2.mail-out.ovh.net
- Ironport-phdr: 9a23:B4gdgRJxFQO+3ju+19mcpTZWNBhigK39O0sv0rFitYgULvnxwZ3uMQTl6Ol3ixeRBMOAuqgC1Led6vq+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuS9SU0Jn8jrrss7ToICxwzAKnZr1zKBjk5S7wjeIxxbVYF6Aq1xHSqWFJcekFjUlhJFaUggqurpzopM0rxQ0L5Klkr5IIEfiiPvdwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09tChjE6Ryychb3MjCy4u902S2yOMTmTLU5VTmk4rwtRgW+23RPDCIw7GyC0p84t6lcuh/0+kRy
Hi Greg,
As a workaround, you can do:
Arguments baz {_ _} !pf _.
On 10/29/16 19:46, Gregory Malecha wrote:
> Hello --
>
> I have three functions that look roughly like this:
>
> Definition foo {a b : Type} (F : Type -> Type) (pf : a = b) : F a -> F b :=
> match pf with
> | eq_refl => fun x => x
> end.
>
> Definition bar {a b : Type} (pf : a = b) : a -> b :=
> @foo a b (fun x => x) pf.
>
> Definition baz {a b : Type} (pf : a = b) : b -> a :=
> @bar b a (eq_sym pf).
>
> I am writing the following annotations for simpl.
>
> Arguments foo {_ _} _ !pf _.
> Arguments bar {_ _} !pf _.
> Arguments baz {_ _} !pf _.
>
> And I get the following behavior:
>
> Eval simpl in @foo nat nat (fun x => x) eq_refl 1. (* = 1 *)
> Eval simpl in @bar nat nat eq_refl 1. (* = 1 *)
> Eval simpl in @baz nat nat eq_refl 1. (* = baz eq_refl 1 *)
>
> The first two of these are exactly what I expect, but the third seems
> wrong. If I understand correctly, the documentation says that baz should
> be reduced if the proof argument is a constructor (which it is:
> eq_refl). Once that unfolds, eq_sym should reduce since it is applied to
> a constructor (just to be sure I added an: Arguments eq_sym {_ _ _}
> !_.), and then bar should reduce and finally foo should reduce.
>
> Is there any work-around that does not involve inlining the definition
> of `foo` inside `baz`?
>
> Thanks.
> --
>
> - gregory malecha
> gmalecha.github.io <http://gmalecha.github.io>
>
- [Coq-Club] simpl should reduce on constructor?, Gregory Malecha, 10/29/2016
- Re: [Coq-Club] simpl should reduce on constructor?, Maxime Dénès, 10/29/2016
- Re: [Coq-Club] simpl should reduce on constructor?, Maxime Dénès, 10/29/2016
- Re: [Coq-Club] simpl should reduce on constructor?, Gregory Malecha, 10/30/2016
- Re: [Coq-Club] simpl should reduce on constructor?, Maxime Dénès, 10/29/2016
- Re: [Coq-Club] simpl should reduce on constructor?, Maxime Dénès, 10/29/2016
Archive powered by MHonArc 2.6.18.