“崩溃”功能图中的状态？

问题描述

该问题的灵感来自软件基础，但与练习无关。到目前为止，我所知道的。

Imp章节（简单命令式程序）使用功能映射（来自 Maps章节（ Total and Partial Maps））用于简化的环境。[1]编程语言。

 归纳ID：类型：= 
 | id：字符串-> ID。 
 
定义total_map（A：Type）：= id-> A. 
 
定义t_empty {A：Type}（v：A）：total_map A：= 
（fun _ => v）。 
 
定义t_update {A：Type}（m：total_map A）（x：id）（v：A）：= 
 fun x’=>如果beq_id x x’，则反之m x’。 
  

在Imp章节中对程序进行推理需要处理 t_update形式的程序状态（t_update（...）x 4）y 12），这变得乏味，因为状态随着每个赋值而增长，即使该赋值正在实现是对现有变量的更新。 / p>

从理论上讲，应该有可能将程序状态折叠为每个变量的单个 t_update 已经证明了几个方向正确的引理。

 需要导入Coq.Logic.FunctionalExtensionality 。 
 
引理swap_updates：forall A（m：total_map A）x vx y vy，
 x< y-> t_update（t_update m x vx）y vy = t_update（t_update m xvy）x vx。 
证明。 
简介A m x vx y vy H.应用functional_extensionality。简介k。 
展开t_update。销毁（beq_id y k）eqn：Eqyk。 
-销毁（beq_id x k）eqn：Eqxk。 
 +在Eqyk中应用beq_id_true_iff。在Eqxk中应用beq_id_true_iff。替代
矛盾。 
 +自反性。 
-销毁（beq_id x k）eqn：Eqxk;自反性。 
 Qed。 
 
引理collapse_updates：全部A（m：total_map A）x v1 v2，
 t_update（t_update m x v1）x v2 = t_update m x v2。 
证明。 
前奏A m x v1 v2。应用functional_extensionality。简介k。 
展开t_update。破坏（beq_id x k）;自反性。 
 Qed。 
  

但是我不知道该如何陈述（就此而言，更少的证明或使用）定理 t_update（...（t_update（...）x 4）...）x 27 等于 t_update（... ）x 27 ;即删除 x 的无用绑定。

有什么想法吗？

[1]我刚刚看到了这个。我要离开了，但我正在考虑尽快从Coq度假。

解决方案

首先，它是不必这样陈述一个定理，就足以解出以下形式的方程

  t_update ...（t_update ...）= t_update ...（t_update ...）
  

实现目标。这是以下自定义策略的作用。

 需要导入Coq.Logic.FunctionalExtensionality。 
 
 Ltac t_solve：= $​​ b $ b简介；应用functional_extensionality；简介；展开t_update; 
用
 |-context [beq_id？v？x] =>重复执行lazymatch目标。 
 case_eq（beq_id v x）; 
 [重写beq_id_true_iff |重写beq_id_false_iff];介绍
结尾； 
替代； （一致性||区分）。 
  

我们知道，如果beq_id，则状态只是嵌套的阶梯。 ？那么... else ... 表达式，所以如果我们破坏所有 beq_id？使用上下文机制的？子表达式，那么一些标准策略很聪明，足以为我们完成工作。如果变量上的数字足够大，则此解决方案将行不通，但应足以通过Software Foundations工作。

This question is inspired by Software Foundations, but isn't about an exercise. That I know about, so far.

The Imp chapter ("Simple Imperative Programs") uses functional maps (from the Maps chapter ("Total and Partial Maps")) for the environment of the simpl.[1] programming language.

Inductive id : Type :=
  | Id : string -> id.

Definition total_map (A:Type) := id -> A.

Definition t_empty {A:Type} (v : A) : total_map A :=
  (fun _ => v).

Definition t_update {A:Type} (m : total_map A) (x : id) (v : A) :=
  fun x' => if beq_id x x' then v else m x'.

Reasoning about programs in the Imp chapter requires manipulating program states of the form t_update (t_update (...) x 4) y 12), which becomes tedious because the state grows with every assignment, even if what the assignment is "implementing" is an update of an existing variable.

In theory, it should be possible to collapse program states down to single t_update's for each variable, and I've gone so far as to prove a couple of lemmas that go in the right direction.

Require Import Coq.Logic.FunctionalExtensionality.

Lemma swap_updates : forall A (m : total_map A) x vx y vy,
  x <> y -> t_update (t_update m x vx) y vy = t_update (t_update m y vy) x vx.
Proof.
  intros A m x vx y vy H. apply functional_extensionality. intros k.
  unfold t_update. destruct (beq_id y k) eqn:Eqyk.
  - destruct (beq_id x k) eqn:Eqxk.
    + apply beq_id_true_iff in Eqyk. apply beq_id_true_iff in Eqxk. subst.
      contradiction.
    + reflexivity.
  - destruct (beq_id x k) eqn:Eqxk; reflexivity.
Qed.

Lemma collapse_updates : forall A (m : total_map A) x v1 v2,
  t_update (t_update m x v1) x v2 = t_update m x v2.
Proof.
  intros A m x v1 v2. apply functional_extensionality. intros k.
  unfold t_update. destruct (beq_id x k); reflexivity.
Qed.

But I don't know how to state (much less prove or use, for that matter) a theorem that t_update (... (t_update (...) x 4) ...) x 27 is equal to t_update (...) x 27; i.e. with the useless bindings for x removed.

Any ideas?

[1] I just saw this. I'm leaving it, but I'm considering taking a vacation from Coq soon.

解决方案

First of all, it's not necessary to state a theorem like that, it's sufficient to be able to solve equations of the form

t_update ... (t_update ...) = t_update ... (t_update ...)

to achieve your goals. This is what does the following custom tactic.

Require Import Coq.Logic.FunctionalExtensionality.

Ltac t_solve :=
  intros; apply functional_extensionality; intros; unfold t_update;
  repeat lazymatch goal with
  |- context [beq_id ?v ?x] =>
    case_eq (beq_id v x);
    [rewrite beq_id_true_iff | rewrite beq_id_false_iff]; intros
  end;
  subst; (congruence || discriminate).

We know that states are just ladders of nested if beq_id ? ? then ... else ... expressions so if we destruct all the beq_id ? ? subexpressions using the context mechanism then some standard tactics are smart enough to finish the work for us. This solution won't work if the number on variables is large enough, but should be sufficient to work through Software Foundations.

这篇关于“崩溃”功能图中的状态？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！