The Coq mailing list

[CJ Bell <siegebell AT gmail.com>]

The problem with my solution is that you must write "|-{P} (1+2) {Q}"
instead of "|-{P} 1+2 {Q}". Parentheses are always required around the
command in the center because of the way that functions are parsed :/


-cj



On Fri, Mar 8, 2013 at 7:07 PM, CJ Bell 
<siegebell AT gmail.com>
 wrote:
> Here is an approach that works because it uses the existing notation
> for " { } " and requires prefixing Hoare triples with "|-" (or some
> other keyword). Hard to tell if it breaks something, though.
>
>
> Inductive ht_pred : Set := ht_pred_: nat->ht_pred.
> Inductive ht : ht_pred->nat->ht_pred->Prop := .
>
> Delimit Scope htriple with htriple.
> Delimit Scope htriple_pred with htriple_pred.
> Arguments ht P%htriple_pred c%nat Q%htriple_pred.
>
> Module Notations.
>   Notation " { P } " := (ht_pred_ P%nat) : htriple_pred.
>   Notation "|-" := ht (no associativity, at level 0) : htriple.
> End Notations.
>
> Module TestNotations.
>   Import Notations.
>   Open Scope htriple.
>
>   (* do existing notations still work? *)
>   Record Rat : Set := mkRat {
>     top: nat; bottom: nat; Rat_cond: (gt bottom O) }.
>   Goal (forall b:bool, { b=true } + { b=false }). destruct b; auto. Qed.
>   Goal {a | a<>false}. exists true; intro; discriminate. Qed.
>
>   Goal (forall p, {p}%htriple_pred = ht_pred_ p). reflexivity. Qed.
>
>   Goal (forall p c q,
>     |- {p} c {q} <-> ht (ht_pred_ p) c (ht_pred_ q)).
>   Proof. split; intros; auto. Qed.
>
> End TestNotations.
>
>
>
> -cj