The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Arnaud,

 

thanks a lot, very helpful!

 

Best regards,

 

Michael

 

From: arnaud.spiwack AT gmail.com [mailto:arnaud.spiwack AT gmail.com] On Behalf Of Arnaud Spiwack
Sent: Monday, February 02, 2015 1:39 PM
To: Coq Club
Subject: Re: [Coq-Club] Applying a simplified hypothesis gives the original hypothesis in the proof term

 

This should be what you are after:

Definition x : list nat.
  let h := constr:([1;2;3] ++ [4;5;6]) in
  let h' := eval compute in h in
  set (H:= h').
  exact H.
Defined.

 

On 2 February 2015 at 10:54, Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Coq users,

when I simplify a hypothesis and then apply it, the proof term contains the original unsimplified hypothesis:

Require Import List.
Open Scope list_scope.
Import ListNotations.

Definition a := [1;2;3].

Definition x : list nat.
  set (H:= [1;2;3] ++ [4;5;6] ).
  compute in H.
  exact H.
Defined.

Print x. (* Results in x = let H := [1; 2; 3] ++ [4; 5; 6] in H : list nat *)

This is a bit inconvenient, especially in connection with the new $( )$ syntax.
Of cause I can use "Eval compute in" or similar outside of $( )$ but in some cases I want to be more selective in how to simplifiy which term.
I wonder if there is a way to get the simplified proof term in the proof term.

Btw.: "Eval compute in" doesn't work with "Instance", which might be a useful feature in connection with $( )$.

Best regards,

Michael