Hi all, I'm currently in the process of trying to separate a computation from a proof. (Specifically, of Hoare proof trees.) I basically have a tree structure that looks something like this:

```
Inductive hoare_tree :=
| HTSkip (P: Assertion) (* has pre/post-condition P *)
| HTAssign (P: Assertion) (x: string) (a: aexp) (* has precondition P[x -> a] and postcondition P *)
| HTSeq (P Q R: Assertion) (i1 i2: imp) (H1 H2: hoare_tree). (* has precondition P, postcondition R *)
```

We can pretend that `Assertion := nat -> Prop`

. (It's a little more complicated than that, but this is the sticking point.)

I'd like to be able to write a checker function for the `hoare_tree`

that would check that the tree is valid. But for `HTSeq`

, for instance, this requires `H1`

to have the precondition `P`

and postcondition `Q`

, and there's no way to check the equality in a decidable way in plain Coq (afaik).

I'm looking into Metacoq to do this using syntactic equality of these Prop functions by quoting them. Are there any other considerations I need to make in order to do this? Is there anything I'm overlooking? Thanks!

you could write a checker which goes `hoare_tree -> Prop`

instead of `-> bool`

, such that the Prop is the necessary conditions for the tree to be valid (False when not possible to be valid)

then on concrete terms you can do something like `cbv beta iota [checker]; tauto`

to prove a `checker`

goal

Last updated: Jun 13 2024 at 19:02 UTC