1
$\begingroup$

Hello Stack Exchange Community,

I'm currently working on my thesis which involves using Interaction Trees to define big-step operational semantics for programming languages, particularly the IMP language. The work done in the DeepSpec/InteractionTrees tutorial has been a significant part of my research foundation.

My current focus is on program transformations and their impact on preserving program semantics, especially in the context of constant folding. However, I've hit a roadblock while attempting to prove the constant folding theorem, specifically the 'while' case. Despite my best efforts, there seems to be an issue with my application of coinduction, which is puzzling considering the design of Interaction Trees to simplify such complexities.

I've extended the tutorial's Coq file to include the constant folding theorem and related definitions.

Fixpoint fold_constants_expr (a : expr) : expr :=
  match a with
  | Var x => Var x
  | Lit n => Lit n
  | Plus a1 a2 =>
    match (fold_constants_expr a1,
           fold_constants_expr a2)
    with
    | (Lit n1, Lit n2) => Lit (n1 + n2)
    | (a1', a2') => Plus a1' a2'
    end
  | Minus a1 a2 =>
    match (fold_constants_expr a1,
           fold_constants_expr a2)
    with
    | (Lit n1, Lit n2) => Lit (n1 - n2)
    | (a1', a2') => Minus a1' a2'
    end
  | Mult a1 a2 =>
    match (fold_constants_expr a1,
           fold_constants_expr a2)
    with
    | (Lit n1, Lit n2) => Lit (n1 * n2)
    | (a1', a2') => Mult a1' a2'
    end
  end.
Fixpoint fold_constants_stmt (s : stmt) : stmt :=
  match s with
  | Assign x e => Assign x (fold_constants_expr e)
  | Seq s1 s2 => Seq (fold_constants_stmt s1) (fold_constants_stmt s2)
  | If e s1 s2 => match fold_constants_expr e with
                  | Lit 0 => fold_constants_stmt s2
                  | Lit _ => fold_constants_stmt s1
                  | e' => If e' (fold_constants_stmt s1) (fold_constants_stmt s2)
                  end
  | While e s => match fold_constants_expr e with
                 | Lit 0 => Skip
                 | Lit (S x) => While (Lit (S x)) (fold_constants_stmt s)
                 | e' => While e' (fold_constants_stmt s)
                 end
  
  | Skip => Skip
  end.

Using the definitions of the tutorial I want to provide the following theorems:

Theorem denote_imp_fold_constants_expr : forall e,
    denote_expr (fold_constants_expr e) ≅ denote_expr e.  
Theorem denote_imp_fold_constants_stmt : forall s,
    denote_imp (fold_constants_stmt s) ≅ denote_imp s.

The first results is pretty easy to prove. The second theorem is also relatively straightforward, except for the while case. I am facing challenges in finalizing the proof and would appreciate any insights or guidance on this matter.

I've tried several approaches but seem to be missing something crucial. Here are some specific aspects I'm struggling with: I have tried using co-induction for the while case, but when I get to the end of the proof, it seems that my use of co-induction is ill-formed.

I am also open to the possibility of an online discussion if anyone is well-versed in this area and willing to help.

Thank you very much for your time and assistance.

$\endgroup$

1 Answer 1

0
$\begingroup$

Having a quick look, it looks like the main issue is that a useful instance for iter seems to be missing from the library, preventing the rewrite (* HERE *) that you would naturally do, and hence forcing you to either retro-engineer this problem, or working around more awkwardly.

Here is a solution building on the Imp.v file from the tutorial. Note that there is no need for coinduction here, both denotations being both iters that are "in lock step". Let me know if anything is unclear, I'm happy to discuss or call in off if it's useful.

EDIT: To expand further, as you mentioned having tried to go through by coinduction. Note that the semantics we provide for Imp is defined recursively on the syntax, crucially thanks to the iter combinator in the case of the while. As such, an induction on the syntax is sufficient, in contrast with what we would get if reasoning w.r.t. a non-compositional semantics, and of course provided we have sufficient reasoning principle about iter.

Here the reasoning principle in question is essentially embodied in eq_itree_iter: if two bodies are pointwise strongly bisimilar, their iterations are as well. We have reduced our goal to comparing bodies, our induction principle is hence sufficient.

Alternate principles are provided for more complex cases. Crucially, one can also reason w.r.t. weak bisimilarity (eutt in the library), that is eutt_iter. Sometimes, indexes of iteration must be remapped, and some of them disagree but to no harm as they are unreachable: eq_itree_iter'/eutt_iter'/eutt_iter'' provide support for it. And sometimes we are out of the clean-cut pathway: for instance if you were to merge two blocks in a semantics like the asm language, you would have to line up one iteration of the loop defining the semantics (at the target, processing one merged block) to two of them (at the source, going consecutively through both blocks). In this case, none of the lemmas above have your back, and you typically resort on cooking up locally your own proof by coinduction (albeit I'm pretty sure we should be able to provide some kind of 1-to-n generic principle at the granularity of body iteration easily, it's not done at the moment).

Finally, note that if you would like to interact with other users/developer, you can do it over the dedicated stream zulip: https://coq.zulipchat.com/#narrow/stream/394939-Interaction-Trees/

Best,

Yannick

Fixpoint fold_constants_expr (a : expr) : expr :=
  match a with
  | Var x => Var x
  | Lit n => Lit n
  | Plus a1 a2 =>
    match (fold_constants_expr a1,
           fold_constants_expr a2)
    with
    | (Lit n1, Lit n2) => Lit (n1 + n2)
    | (a1', a2') => Plus a1' a2'
    end
  | Minus a1 a2 =>
    match (fold_constants_expr a1,
           fold_constants_expr a2)
    with
    | (Lit n1, Lit n2) => Lit (n1 - n2)
    | (a1', a2') => Minus a1' a2'
    end
  | Mult a1 a2 =>
    match (fold_constants_expr a1,
           fold_constants_expr a2)
    with
    | (Lit n1, Lit n2) => Lit (n1 * n2)
    | (a1', a2') => Mult a1' a2'
    end
  end.

Fixpoint fold_constants_stmt (s : stmt) : stmt :=
  match s with
  | Assign x e => Assign x (fold_constants_expr e)
  | Seq s1 s2 => Seq (fold_constants_stmt s1) (fold_constants_stmt s2)
  | If e s1 s2 => match fold_constants_expr e with
                  | Lit 0 => fold_constants_stmt s2
                  | Lit _ => fold_constants_stmt s1
                  | e' => If e' (fold_constants_stmt s1) (fold_constants_stmt s2)
                  end
  | While e s => match fold_constants_expr e with
                 | Lit 0 => Skip
                 | Lit (S x) => While (Lit (S x)) (fold_constants_stmt s)
                 | e' => While e' (fold_constants_stmt s)
                 end

  | Skip => Skip
  end.

Theorem denote_imp_fold_constants_expr : forall e,
    denote_expr (eff := ImpState) (fold_constants_expr e) ≅ denote_expr e.
Proof.
  intros e; induction e; try reflexivity.
  all: cbn; setoid_rewrite <- IHe1; setoid_rewrite <- IHe2.
  all: destruct (fold_constants_expr e1) eqn:Eq1, (fold_constants_expr e2) eqn:Eq2.
  all: cbn; try reflexivity.
  all: now rewrite ?bind_ret_l.
Qed.

Ltac bind := eapply eq_itree_clo_bind; [reflexivity | intros ? ? <-].

(* This is what tripped me: without this instance, the rewrite marked as "HERE" in the proof below fails, forcing you to work around awkwardly otherwise *)
#[global] Instance missing_iter_instance {E R I}:
  Proper (pointwise_relation I (eq_itree eq) ==> eq ==> eq_itree eq) (@ITree.iter E R I).
Proof.
  repeat intro.
  subst; eapply eq_itree_iter; intros ?? <-; apply H.
Qed.

Theorem denote_imp_fold_constants_stmt : forall s,
    denote_imp (eff := ImpState) (fold_constants_stmt s) ≅ denote_imp s.
Proof.
  intros s; induction s.
  - cbn; now rewrite denote_imp_fold_constants_expr.
  - cbn. now setoid_rewrite IHs1; setoid_rewrite IHs2.
  - cbn.
    rewrite <- (denote_imp_fold_constants_expr i).
    destruct (fold_constants_expr i) eqn:eqi.
    all: cbn.
    all: try bind.
    all: try now case is_true; eauto.
    destruct v; subst; rewrite bind_ret_l.
    now cbn; rewrite IHs2.
    now cbn; rewrite IHs1.
  - assert (BASE_CASE: forall (t : expr),
               denote_imp (eff := ImpState) (WHILE (fold_constants_expr t) DO (fold_constants_stmt s)) ≅
               denote_imp (WHILE t DO s)
           ).
    { clear t; intros t.
      cbn.
      eapply eq_itree_iter; intros ?? <-.
      try (rewrite denote_imp_fold_constants_expr; bind).
      case is_true; try reflexivity.
      try now rewrite IHs.
    }
    cbn.
    destruct (fold_constants_expr t) eqn:eqt; [| destruct v |..];
      try (rewrite <- eqt; apply BASE_CASE).
    cbn.
    unfold while.
    (* HERE *)
    setoid_rewrite <- (denote_imp_fold_constants_expr t).
    rewrite eqt.
    cbn.
    rewrite unfold_iter_ktree.
    rewrite ? bind_ret_l.
    now cbn; rewrite ? bind_ret_l.
  - reflexivity.
Qed.
$\endgroup$
1
  • $\begingroup$ Thank you very much, Yannick! Your solution perfectly addresses the rewrite issue I was facing with the constant folding theorem. The missing_iter_instance was particularly enlightening, and your explanation has significantly deepened my understanding of the ITrees library's capabilities. I greatly appreciate your detailed and insightful response. Thanks again! $\endgroup$ Dec 9, 2023 at 14:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.