diff options
Diffstat (limited to 'main.org')
| -rw-r--r-- | main.org | 26 |
1 files changed, 26 insertions, 0 deletions
@@ -82,6 +82,18 @@ final expression tree. Speaking of the tree, we can also define the forest that from resource to corresponding expression. #+begin_src coq +Definition predicate := positive. +Definition pred_op := @Predicate.pred_op predicate. +Definition predicated A := NE.non_empty (pred_op * A). +Definition pred_expr := predicated expression. + +Definition apred : Type := expression. +Definition apred_op := @Predicate.pred_op apred. +Definition apredicated A := NE.non_empty (apred_op * A). +Definition apred_expr := apredicated expression. +#+end_src + +#+begin_src coq <<R_indexed-def>> Module Rtree := ITree(R_indexed). Definition forest : Type := Rtree.t apred_expr. @@ -90,6 +102,13 @@ Definition forest : Type := Rtree.t apred_expr. where ~R_indexed~ is a proof of injectivity from resources into the positives, and is further defined in the [[R_indexed-def-link][next section]]. +Finally, lets assume that we have a correct syntactic equality check between two expressions, so +that we can get a decidable equality check between expressions. + +#+begin_src coq +Axiom expression_dec: forall e1 e2: expression, {e1 = e2} + {e1 <> e2}. +#+end_src + ** Definition of R_indexed :PROPERTIES: :CUSTOM_ID: R_indexed-def-link @@ -127,6 +146,7 @@ Module R_indexed. <<R_indexed-injectivity>> End R_indexed. #+end_src +* First Attempt at Symbolic Analysis * Top-level imports :PROPERTIES: @@ -158,8 +178,14 @@ Require Import vericert.hls.HashTree. Require Import vericert.hls.Predicate. Require Import vericert.common.DecEq. +Require symb.NonEmpty. + +Module NE := NonEmpty. +Import NE.NonEmptyNotation. + #[local] Open Scope positive. #[local] Open Scope pred_op. +#[local] Open Scope non_empty_scope. #+end_src * Footnotes |