Machine-Checked Mathematics

Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line. Use ALT-(right-arrow) to go to the cursor. You can save your edits inside your browser and load them back. Finally, you can download your working copy of the file, e.g., for sending it to teachers.

Exercise 1:

Improve the last symplification function of lesson 5 by adding the simplification rule $$x - 0 = x$$

Module Ex1.

Inductive expr :=
  | Zero
  | Minus (x : expr) (y : expr)
  | Var (n : nat).

Fixpoint interp (e : expr) (c : list nat) :=
  match e with
  | Zero => 0
  | Minus x y => (interp x c) - (interp y c)
  | Var x => nth 0 c x
  end.

Lemma simplify_correct (e : expr) (c : list nat) : interp e c = interp (simplify e) c.
Proof.
elim: e => //= x Hx y Hy.
case: (simplify x) Hx => [|x1 x2|n] -> ; case: (simplify y) Hy => [|y1 y2|m] -> //.
(* fill in *)
1,2: by rewrite subn0.
by case: eqP => [->|//]; rewrite subnn.
Qed.

Lemma test (x : nat) : x - x - 0 = 0.
Proof.
pose AST : expr := Minus (Minus (Var 0) (Var 0)) Zero.
pose CTX : list nat := [:: x].
rewrite -[LHS]/(interp AST CTX).
rewrite simplify_correct.
rewrite /=.
by [].
Qed.

End Ex1.

Exercise 2:

Improve on exercise 1 by adding to the expr inductive type a constructor for multiplication and the simplification rules $$x * 0 = 0$$ and $$0 * x = 0$$

Module Ex2.

Inductive expr :=
  | Zero
  | (* fill in *)
 Mult (x : expr) (y : expr)
  | Minus (x : expr) (y : expr)
  | Var (n : nat).

Fixpoint interp (e : expr) (c : list nat) :=
  match e with
  | Zero => 0
  | Minus x y => (interp x c) - (interp y c)
  | (* fill in *)
 Mult x y => (interp x c) * (interp y c)
  | Var x => nth 0 c x
  end.

Lemma simplify_correct (e : expr) (c : list nat) : interp e c = interp (simplify e) c.
Proof.
elim: e => //= x Hx y Hy.
- case: (simplify x) Hx => [|x1 x2|x1 x2|n] -> ; case: (simplify y) Hy => [|y1 y2|y1 y2|m] -> //.
  (* fill in *)
 1,2,3: by rewrite muln0.
- case: (simplify x) Hx => [|x1 x2|x1 x2|n] -> ; case: (simplify y) Hy => [|y1 y2|y1 y2|m] -> //.
  (* fill in, like in exercise 1 *)
 1,2,3: by rewrite subn0.
  by case: eqP => [->|//]; rewrite subnn.
Qed.

Lemma test (x : nat) (y : nat) : x - x - (y * 0) = 0.
Proof.
pose AST : expr := (* fill me *)
Minus (Minus (Var 0) (Var 0)) (Mult (Var 1) Zero).
pose CTX : list nat := (* fill me *)
[:: x; y].
rewrite -[LHS]/(interp AST CTX).
rewrite simplify_correct.
rewrite /=.
by [].
Qed.

End Ex2.

Exercise 3:

Improve on exercise 2 by adding to the expr data type a constructor for One and the simplification rules $$x * 1 = x$$ and $$1 * x = x$$

Module Ex3.

Lemma simplify_correct (e : expr) (c : list nat) : interp e c = interp (simplify e) c.
Proof.
elim: e => //= x Hx y Hy.
- case: (simplify x) Hx => [||x1 x2|x1 x2|n] -> ; case: (simplify y) Hy => [||y1 y2|y1 y2|m] -> //.
  (* fill in *)
 1,2,3: by rewrite mul1n.
 1,3,5: by rewrite muln0.
 1,2,3: by rewrite muln1.
- case: (simplify x) Hx => [||x1 x2|x1 x2|n] -> ; case: (simplify y) Hy => [||y1 y2|y1 y2|m] -> //.
  (* fill in *)
 1,2,3: by rewrite subn0.
 by case: eqP => [->|//]; rewrite subnn.
Qed.

End Ex3.

(*
</div>

</div>
----------------------------------------------------------
*)