coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs
Date: Thu, 3 Mar 2016 22:23:18 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:IBC8KRwG0Y0kiOnXCy+O+j09IxM/srCxBDY+r6Qd0ekXIJqq85mqBkHD//Il1AaPBtWEra0YwLON4ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6NyZvrnLnpqtX6WEZhunmUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF61738SGkcLlBUAVwrY6h7SW4/w9zDlrax6wibMbp6+dqw9RTn3t/QjcxTvkipSbzM=

Hi,

> On 03/03/2016 02:03 PM, Ralf Jung wrote:
>> Lemma lem1 ... :
>> HoareTriple ... (Lam _ "x" (...)) ...
>
> Are you running 8.5?

Yes.

> Maybe Jonathan can provide a fancy example of tactics-in-terms? :)

All my experiments with tactics-in-terms lead to the same trouble as
plain eq_refl: The tactic is run before the contexts are propagated
down, so things don't work. But it may well be that I did this wrong; I
have yet to see a successful use of tactics-in-terms ;-)

Kind regards,
Ralf

[Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Jonathan Leivent, 03/03/2016
  - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
    - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
      - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Robbert Krebbers, 03/03/2016
  - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Robbert Krebbers, 03/03/2016
    - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
      - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/04/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Gregory Malecha, 03/05/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/06/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Jonathan Leivent, 03/06/2016