feat: 3234 week 5 wip
This commit is contained in:
parent
d9315b13c4
commit
ae3f11405c
35
cs3234/labs/week-05_eqn-and-remember.v
Normal file
35
cs3234/labs/week-05_eqn-and-remember.v
Normal file
@ -0,0 +1,35 @@
|
||||
(* week-05_eqn-and-remember.v *)
|
||||
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
|
||||
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
|
||||
(* Version of 16 Feb 2024 *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Lemma O_or_S :
|
||||
forall n : nat,
|
||||
n = 0 \/ exists n' : nat, n = S n'.
|
||||
Proof.
|
||||
intro n.
|
||||
case n as [ | n'] eqn:H_n.
|
||||
- left.
|
||||
reflexivity.
|
||||
- right.
|
||||
exists n'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Lemma add_1_r :
|
||||
forall n : nat,
|
||||
n + 1 = S n.
|
||||
Proof.
|
||||
intro n.
|
||||
remember (n + 1) as n_plus_1 eqn:H_n_plus_1.
|
||||
remember (S n) as Sn eqn:H_Sn.
|
||||
remember (n_plus_1 = Sn) as prove_me eqn:goal.
|
||||
Abort.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* end of week-05_eqn-and-remember.v *)
|
||||
@ -0,0 +1,644 @@
|
||||
(* week-05_induction-and-induction-proofs-a-recapitulation.v *)
|
||||
(* LPP 2024 - CS3234 2023-2024, Sem2 *)
|
||||
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
|
||||
(* Version of 16 Feb 2024 *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Paraphernalia: *)
|
||||
|
||||
Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
|
||||
|
||||
Require Import Arith Bool.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive bool' : Type :=
|
||||
true' : bool'
|
||||
| false' : bool'.
|
||||
|
||||
(*
|
||||
bool' is defined
|
||||
bool'_rect is defined
|
||||
bool'_ind is defined
|
||||
bool'_rec is defined
|
||||
*)
|
||||
|
||||
Check bool'_ind.
|
||||
(* : forall P : bool' -> Prop, P true' -> P false' -> forall b : bool', P b *)
|
||||
|
||||
Proposition bool'_identity :
|
||||
forall b : bool',
|
||||
b = b.
|
||||
Proof.
|
||||
intro b.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intro b.
|
||||
case b as [ | ] eqn:H_b.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros [ | ].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive nat' : Type :=
|
||||
O'
|
||||
| S' : nat' -> nat'.
|
||||
|
||||
(*
|
||||
nat' is defined
|
||||
nat'_rect is defined
|
||||
nat'_ind is defined
|
||||
nat'_rec is defined
|
||||
*)
|
||||
|
||||
Check nat'_ind.
|
||||
(* : forall P : nat' -> Prop, P O' -> (forall n : nat', P n -> P (S' n)) -> forall n : nat', P n *)
|
||||
|
||||
Proposition nat'_identity :
|
||||
forall n : nat',
|
||||
n = n.
|
||||
Proof.
|
||||
intro n.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intro n.
|
||||
case n as [ | n'] eqn:H_n.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros [ | n'].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intro n.
|
||||
induction n as [ | n' IHn'].
|
||||
-
|
||||
(* The goal is the base case, where "P x" is "x = x", for any x:
|
||||
|
||||
============================
|
||||
O' = O'
|
||||
*)
|
||||
reflexivity.
|
||||
-
|
||||
(*
|
||||
n' : nat
|
||||
IHn' : n' = n'
|
||||
============================
|
||||
S' n' = S' n'
|
||||
*)
|
||||
revert n' IHn'.
|
||||
(* The goal is the induction step, where "P x" is "x = x", for any x:
|
||||
|
||||
============================
|
||||
forall n' : nat', n' = n' -> S' n' = S' n'
|
||||
*)
|
||||
intros n' IHn'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Check nat_ind.
|
||||
(* : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *)
|
||||
|
||||
Proposition nat_identity :
|
||||
forall n : nat,
|
||||
n = n.
|
||||
Proof.
|
||||
intro n.
|
||||
induction n as [ | n' IHn'].
|
||||
-
|
||||
(* The goal is the base case, where "P x" is "x = x", for any x:
|
||||
|
||||
============================
|
||||
0 = 0
|
||||
*)
|
||||
reflexivity.
|
||||
-
|
||||
(*
|
||||
n' : nat
|
||||
IHn' : n' = n'
|
||||
============================
|
||||
S n' = S n'
|
||||
*)
|
||||
revert n' IHn'.
|
||||
(* The goal is the induction step, where "P x" is "x = x", for any x:
|
||||
|
||||
============================
|
||||
forall n' : nat, n' = n' -> S n' = S n'
|
||||
*)
|
||||
intros n' IHn'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive binary_tree_wpl (V : Type) : Type :=
|
||||
Leaf_wpl : V -> binary_tree_wpl V
|
||||
| Node_wpl : binary_tree_wpl V -> binary_tree_wpl V -> binary_tree_wpl V.
|
||||
|
||||
(*
|
||||
binary_tree_wpl is defined
|
||||
binary_tree_wpl_rect is defined
|
||||
binary_tree_wpl_ind is defined
|
||||
binary_tree_wpl_rec is defined
|
||||
*)
|
||||
|
||||
Check binary_tree_wpl_ind.
|
||||
(* : forall (V : Type)
|
||||
(P : binary_tree_wpl V -> Prop),
|
||||
(forall v : V, P (Leaf_wpl V v)) ->
|
||||
(forall t1 : binary_tree_wpl V, P t1 -> forall t2 : binary_tree_wpl V, P t2 -> P (Node_wpl V t1 t2)) ->
|
||||
forall t : binary_tree_wpl V,
|
||||
P t
|
||||
*)
|
||||
|
||||
Proposition binary_tree_wpl_identity :
|
||||
forall (V : Type)
|
||||
(t : binary_tree_wpl V),
|
||||
t = t.
|
||||
Proof.
|
||||
intros V t.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V t.
|
||||
case t as [v | t1 t2] eqn:H_t.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V [v | t1 t2].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
induction t as [v | t1 IHt1 t2 IHt2].
|
||||
- revert v.
|
||||
(* The goal is the base case, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
forall v : V, Leaf_wpl V v = Leaf_wpl V v
|
||||
*)
|
||||
intro v.
|
||||
reflexivity.
|
||||
- revert t1 IHt1 t2 IHt2.
|
||||
(* The goal is the induction step, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
forall t1 : binary_tree_wpl V, t1 = t1 -> forall t2 : binary_tree_wpl V, t2 = t2 -> Node_wpl V t1 t2 = Node_wpl V t1 t2
|
||||
*)
|
||||
intros t1 IHt1 t2 IHt2.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive binary_tree_wpn (V : Type) : Type :=
|
||||
Leaf_wpn : binary_tree_wpn V
|
||||
| Node_wpn : binary_tree_wpn V -> V -> binary_tree_wpn V -> binary_tree_wpn V.
|
||||
|
||||
(*
|
||||
binary_tree_wpn is defined
|
||||
binary_tree_wpn_rect is defined
|
||||
binary_tree_wpn_ind is defined
|
||||
binary_tree_wpn_rec is defined
|
||||
*)
|
||||
|
||||
Check binary_tree_wpn_ind.
|
||||
(* : forall (V : Type)
|
||||
(P : binary_tree_wpn V -> Prop),
|
||||
P (Leaf_wpn V) ->
|
||||
(forall t1 : binary_tree_wpn V,
|
||||
P t1 ->
|
||||
forall (v : V)
|
||||
(t2 : binary_tree_wpn V_,
|
||||
P t2 ->
|
||||
P (Node_wpn V t1 v t2)) ->
|
||||
forall t : binary_tree_wpn V,
|
||||
P t
|
||||
*)
|
||||
|
||||
Proposition binary_tree_wpn_identity :
|
||||
forall (V : Type)
|
||||
(t : binary_tree_wpn V),
|
||||
t = t.
|
||||
Proof.
|
||||
intros V t.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V t.
|
||||
case t as [ | t1 v t2] eqn:H_t.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V [ | t1 v t2].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V t.
|
||||
induction t as [ | t1 IHt1 v t2 IHt2].
|
||||
-
|
||||
(* The goal is the base case, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
Leaf_wpn V = Leaf_wpn V
|
||||
*)
|
||||
reflexivity.
|
||||
- revert t1 IHt1 v t2 IHt2.
|
||||
(* The goal is the induction step, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
forall t1 : binary_tree_wpn V, t1 = t1 -> forall (v : V) (t2 : binary_tree_wpn V), t2 = t2 -> Node_wpn V t1 v t2 = Node_wpn V t1 v t2
|
||||
*)
|
||||
intros t1 IHt1 v t2 IHt2.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive tree3 (V : Type) : Type :=
|
||||
Node0 : V -> tree3 V
|
||||
| Node1 : tree3 V -> tree3 V
|
||||
| Node2 : tree3 V -> tree3 V -> tree3 V
|
||||
| Node3 : tree3 V -> tree3 V -> tree3 V -> tree3 V.
|
||||
|
||||
Proposition tree3_identity :
|
||||
forall (V : Type)
|
||||
(t : tree3 V),
|
||||
t = t.
|
||||
Proof.
|
||||
intros V t.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V t.
|
||||
case t as [v | t1 | t1 t2 | t1 t2 t3] eqn:H_t.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V [v | t1 | t1 t2 | t1 t2 t3].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V t.
|
||||
induction t as [v | t1 IHt1 | t1 IHt1 t2 IHt2 | t1 IHt1 t2 IHt2 t3 IHt3].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive list' (V : Type) : Type :=
|
||||
nil' : list' V
|
||||
| cons' : V -> list' V -> list' V.
|
||||
|
||||
(*
|
||||
list' is defined
|
||||
list'_rect is defined
|
||||
list'_ind is defined
|
||||
list'_rec is defined
|
||||
*)
|
||||
|
||||
Check list'_ind.
|
||||
(* : forall (V : Type)
|
||||
(P : list' V -> Prop),
|
||||
P (nil' V) ->
|
||||
(forall (v : V)
|
||||
(vs' : list' V),
|
||||
P vs' ->
|
||||
P (cons' V v vs')) ->
|
||||
forall vs : list' V,
|
||||
P vs
|
||||
*)
|
||||
|
||||
Proposition list'_identity :
|
||||
forall (V : Type)
|
||||
(vs : list' V),
|
||||
vs = vs.
|
||||
Proof.
|
||||
intros V vs.
|
||||
induction vs as [ | v vs' IHvs'].
|
||||
-
|
||||
(* The goal is the base case, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
nil' V = nil' V
|
||||
*)
|
||||
reflexivity.
|
||||
- revert v vs' IHvs'.
|
||||
(* The goal is the induction step, where "P x" is "x = x", for any x:
|
||||
|
||||
forall (v : V) (vs' : list' V), vs' = vs' -> cons' V v vs' = cons' V v vs'
|
||||
*)
|
||||
intros v vs' IHvs'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Check list_ind.
|
||||
(* : forall (V : Type)
|
||||
(P : list V -> Prop),
|
||||
P nil ->
|
||||
(forall (v : V)
|
||||
(vs' : list V),
|
||||
P vs' ->
|
||||
P (v :: vs)%list) ->
|
||||
forall vs : list V,
|
||||
P vs
|
||||
*)
|
||||
|
||||
Proposition list_identity :
|
||||
forall (V : Type)
|
||||
(vs : list V),
|
||||
vs = vs.
|
||||
Proof.
|
||||
intros V vs.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V vs.
|
||||
case vs as [ | v vs'] eqn:H_vs.
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros V [ | v vs'].
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
|
||||
Restart.
|
||||
intros V vs.
|
||||
induction vs as [ | v vs' IHvs'].
|
||||
-
|
||||
(* The goal is the base case, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
nil = nil
|
||||
*)
|
||||
reflexivity.
|
||||
- revert v vs' IHvs'.
|
||||
(* The goal is the induction step, where "P x" is "x = x", for any x:
|
||||
|
||||
V : Type
|
||||
============================
|
||||
forall (v : V) (vs' : list V), vs' = vs' -> (v :: vs')%list = (v :: vs')%list
|
||||
*)
|
||||
intros v vs' IHvs'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* Exercise 11 *)
|
||||
|
||||
Inductive tsil' (V : Type) : Type :=
|
||||
lin' : tsil' V
|
||||
| snoc' : tsil' V -> V -> tsil' V.
|
||||
|
||||
Fixpoint list'_to_tsil' (V : Type) (vs : list' V) : tsil' V :=
|
||||
match vs with
|
||||
| nil' _ =>
|
||||
lin' V
|
||||
| cons' _ v vs' =>
|
||||
snoc' V (list'_to_tsil' V vs') v
|
||||
end.
|
||||
|
||||
Lemma fold_unfold_list'_to_tsil'_nil' :
|
||||
forall (V : Type),
|
||||
list'_to_tsil' V (nil' V) =
|
||||
lin' V.
|
||||
Proof.
|
||||
fold_unfold_tactic list'_to_tsil'.
|
||||
Qed.
|
||||
|
||||
Lemma fold_unfold_list'_to_tsil'_cons' :
|
||||
forall (V : Type)
|
||||
(v : V)
|
||||
(vs' : list' V),
|
||||
list'_to_tsil' V (cons' V v vs') =
|
||||
snoc' V (list'_to_tsil' V vs') v.
|
||||
Proof.
|
||||
fold_unfold_tactic list'_to_tsil'.
|
||||
Qed.
|
||||
|
||||
Fixpoint tsil'_to_list' (V : Type) (sv : tsil' V) : list' V :=
|
||||
match sv with
|
||||
| lin' _ =>
|
||||
nil' V
|
||||
| snoc' _ sv' v =>
|
||||
cons' V v (tsil'_to_list' V sv')
|
||||
end.
|
||||
|
||||
Lemma fold_unfold_tsil'_to_list'_lin' :
|
||||
forall (V : Type),
|
||||
tsil'_to_list' V (lin' V) =
|
||||
nil' V.
|
||||
Proof.
|
||||
fold_unfold_tactic tsil'_to_list'.
|
||||
Qed.
|
||||
|
||||
Lemma fold_unfold_tsil'_to_list'_snoc' :
|
||||
forall (V : Type)
|
||||
(sv' : tsil' V)
|
||||
(v : V),
|
||||
tsil'_to_list' V (snoc' V sv' v) =
|
||||
cons' V v (tsil'_to_list' V sv').
|
||||
Proof.
|
||||
fold_unfold_tactic tsil'_to_list'.
|
||||
Qed.
|
||||
|
||||
Theorem tsil'_to_list'_is_a_left_inverse_of_list'_to_tsil' :
|
||||
forall (V : Type)
|
||||
(vs : list' V),
|
||||
tsil'_to_list' V (list'_to_tsil' V vs) = vs.
|
||||
Proof.
|
||||
intros V vs.
|
||||
induction vs as [ | v vs' IHvs'].
|
||||
- rewrite -> (fold_unfold_list'_to_tsil'_nil' V).
|
||||
exact (fold_unfold_tsil'_to_list'_lin' V).
|
||||
- rewrite -> (fold_unfold_list'_to_tsil'_cons' V v vs').
|
||||
rewrite -> (fold_unfold_tsil'_to_list'_snoc' V (list'_to_tsil' V vs') v).
|
||||
rewrite -> IHvs'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Theorem list'_to_tsil'_is_a_left_inverse_of_tsil'_to_list' :
|
||||
forall (V : Type)
|
||||
(sv : tsil' V),
|
||||
list'_to_tsil' V (tsil'_to_list' V sv) = sv.
|
||||
Proof.
|
||||
intros V sv.
|
||||
induction sv as [ | sv' IHsv' v].
|
||||
- rewrite -> (fold_unfold_tsil'_to_list'_lin' V).
|
||||
exact (fold_unfold_list'_to_tsil'_nil' V).
|
||||
- rewrite -> (fold_unfold_tsil'_to_list'_snoc' V sv' v).
|
||||
rewrite -> (fold_unfold_list'_to_tsil'_cons' V v (tsil'_to_list' V sv')).
|
||||
rewrite -> IHsv'.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Theorem identity :
|
||||
forall (V : Type)
|
||||
(v : V),
|
||||
v = v.
|
||||
Proof.
|
||||
intros V v.
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
Corollary list_identity_revisited :
|
||||
forall (V : Type)
|
||||
(vs : list V),
|
||||
vs = vs.
|
||||
Proof.
|
||||
intro V.
|
||||
exact (identity (list V)).
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition bool_to_bool' (b : bool) : bool' :=
|
||||
match b with
|
||||
| true =>
|
||||
true'
|
||||
| false =>
|
||||
false'
|
||||
end.
|
||||
|
||||
Definition bool'_to_bool (b : bool') : bool :=
|
||||
match b with
|
||||
| true' =>
|
||||
true
|
||||
| false' =>
|
||||
false
|
||||
end.
|
||||
|
||||
Proposition bool'_to_bool_is_a_left_inverse_of_bool_to_bool' :
|
||||
forall b : bool,
|
||||
bool'_to_bool (bool_to_bool' b) = b.
|
||||
Proof.
|
||||
intro b.
|
||||
case b.
|
||||
- rewrite→ (bool_to_bool' true).
|
||||
intros [ | ].
|
||||
- reflexivity.
|
||||
intros [ | ]; reflexivity.
|
||||
Qed.
|
||||
|
||||
Proposition bool_to_bool'_is_a_left_inverse_of_bool'_to_bool :
|
||||
forall b' : bool',
|
||||
bool_to_bool' (bool'_to_bool b') = b'.
|
||||
Proof.
|
||||
intros [ | ]; reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive byte_code_instruction : Type :=
|
||||
PUSH : nat -> byte_code_instruction
|
||||
| ADD : byte_code_instruction
|
||||
| SUB : byte_code_instruction.
|
||||
|
||||
Inductive target_program : Type :=
|
||||
Target_program : list byte_code_instruction -> target_program.
|
||||
|
||||
Proposition target_program_identity :
|
||||
forall sp : target_program,
|
||||
sp = sp.
|
||||
Proof.
|
||||
intro sp.
|
||||
(*
|
||||
sp : target_program
|
||||
============================
|
||||
sp = sp
|
||||
*)
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros [bcis].
|
||||
(*
|
||||
bcis : list byte_code_instruction
|
||||
============================
|
||||
Target_program bcis = Target_program bcis
|
||||
*)
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros [[ | bci bcis']].
|
||||
(*
|
||||
============================
|
||||
Target_program nil = Target_program nil
|
||||
|
||||
subgoal 2 (ID 36) is:
|
||||
Target_program (bci :: bcis') = Target_program (bci :: bcis')
|
||||
*)
|
||||
- reflexivity.
|
||||
- reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Inductive empty : Type.
|
||||
|
||||
Proposition empty_identity :
|
||||
forall e : empty,
|
||||
e = e.
|
||||
Proof.
|
||||
intro e.
|
||||
reflexivity.
|
||||
|
||||
Restart.
|
||||
|
||||
intros [].
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* end of week-05_induction-and-induction-proofs-a-recapitulation.v *)
|
||||
223
cs3234/labs/week-05_reasoning-about-lambda-dropped-functions.v
Normal file
223
cs3234/labs/week-05_reasoning-about-lambda-dropped-functions.v
Normal file
@ -0,0 +1,223 @@
|
||||
(* week-05_reasoning-about-lambda-dropped-functions.v *)
|
||||
(* LPP 2024 - CS3235 2023-2024, Sem2 *)
|
||||
(* Olivier Danvy <danvy@yale-nus.edu.sg> *)
|
||||
(* Version of 16 Feb 2024 *)
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Ltac fold_unfold_tactic name := intros; unfold name; fold name; reflexivity.
|
||||
|
||||
Require Import Arith Bool List.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition add_acc (n m : nat) : nat :=
|
||||
let fix loop n a :=
|
||||
match n with
|
||||
O =>
|
||||
a
|
||||
| S n' =>
|
||||
loop n' (S a)
|
||||
end
|
||||
in loop n m.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Lemma O_is_right_neutral_for_add_acc :
|
||||
forall n : nat,
|
||||
add_acc n 0 = n.
|
||||
Proof.
|
||||
unfold add_acc.
|
||||
remember (fix loop (n0 a : nat) {struct n0} : nat := match n0 with
|
||||
| 0 => a
|
||||
| S n' => loop n' (S a)
|
||||
end)
|
||||
as loop eqn:H_loop.
|
||||
assert (fold_unfold_loop_O :
|
||||
forall a : nat,
|
||||
loop 0 a = a).
|
||||
{ intro a.
|
||||
rewrite -> H_loop.
|
||||
reflexivity. }
|
||||
assert (fold_unfold_loop_S :
|
||||
forall n' a : nat,
|
||||
loop (S n') a = loop n' (S a)).
|
||||
{ intros n' a.
|
||||
rewrite -> H_loop.
|
||||
reflexivity. }
|
||||
assert (about_loop :
|
||||
forall n a : nat,
|
||||
loop n a = loop n 0 + a).
|
||||
{ intro n'.
|
||||
induction n' as [ | n'' IHn'']; intro a.
|
||||
- rewrite -> (fold_unfold_loop_O a).
|
||||
rewrite -> (fold_unfold_loop_O 0).
|
||||
exact (Nat.add_0_l a).
|
||||
- rewrite -> (fold_unfold_loop_S n'' a).
|
||||
rewrite -> (fold_unfold_loop_S n'' 0).
|
||||
rewrite (IHn'' (S a)).
|
||||
rewrite (IHn'' (S 0)).
|
||||
Check Nat.add_assoc.
|
||||
rewrite <- Nat.add_assoc.
|
||||
Check Nat.add_1_l.
|
||||
rewrite -> (Nat.add_1_l a).
|
||||
reflexivity. }
|
||||
intro n.
|
||||
induction n as [ | n' IHn'].
|
||||
- rewrite -> (fold_unfold_loop_O 0).
|
||||
reflexivity.
|
||||
- rewrite -> (fold_unfold_loop_S n' 0).
|
||||
rewrite -> (about_loop n' 1).
|
||||
rewrite -> IHn'.
|
||||
exact (Nat.add_1_r n').
|
||||
Qed.
|
||||
|
||||
(* ***** *)
|
||||
|
||||
Lemma add_acc_is_associative :
|
||||
forall n1 n2 n3 : nat,
|
||||
add_acc n1 (add_acc n2 n3) = add_acc (add_acc n1 n2) n3.
|
||||
Proof.
|
||||
unfold add_acc.
|
||||
remember (fix loop (n0 a : nat) {struct n0} : nat := match n0 with
|
||||
| 0 => a
|
||||
| S n' => loop n' (S a)
|
||||
end)
|
||||
as loop eqn:H_loop.
|
||||
assert (fold_unfold_loop_O :
|
||||
forall a : nat,
|
||||
loop 0 a = a).
|
||||
{ intro a.
|
||||
rewrite -> H_loop.
|
||||
reflexivity. }
|
||||
assert (fold_unfold_loop_S :
|
||||
forall n' a : nat,
|
||||
loop (S n') a = loop n' (S a)).
|
||||
{ intros n' a.
|
||||
rewrite -> H_loop.
|
||||
reflexivity. }
|
||||
assert (about_loop :
|
||||
forall n a : nat,
|
||||
loop n a = loop n 0 + a).
|
||||
{ intro n'.
|
||||
induction n' as [ | n'' IHn'']; intro a.
|
||||
- rewrite -> (fold_unfold_loop_O a).
|
||||
rewrite -> (fold_unfold_loop_O 0).
|
||||
exact (Nat.add_0_l a).
|
||||
- rewrite -> (fold_unfold_loop_S n'' a).
|
||||
rewrite -> (fold_unfold_loop_S n'' 0).
|
||||
rewrite (IHn'' (S a)).
|
||||
rewrite (IHn'' (S 0)).
|
||||
Check Nat.add_assoc.
|
||||
rewrite <- Nat.add_assoc.
|
||||
Check Nat.add_1_l.
|
||||
rewrite -> (Nat.add_1_l a).
|
||||
reflexivity. }
|
||||
intro n1.
|
||||
induction n1 as [ | n1' IHn1'].
|
||||
- intros n2 n3.
|
||||
rewrite -> (fold_unfold_loop_O (loop n2 n3)).
|
||||
rewrite -> (fold_unfold_loop_O n2).
|
||||
reflexivity.
|
||||
- intros n2 n3.
|
||||
rewrite -> (fold_unfold_loop_S n1' (loop n2 n3)).
|
||||
rewrite -> (fold_unfold_loop_S n1' n2).
|
||||
rewrite <- (IHn1' (S n2) n3).
|
||||
assert (helpful :
|
||||
forall x y : nat,
|
||||
S (loop x y) = loop (S x) y).
|
||||
{ intro x.
|
||||
induction x as [ | x' IHx'].
|
||||
- intro y.
|
||||
rewrite -> (fold_unfold_loop_O y).
|
||||
rewrite -> (fold_unfold_loop_S 0 y).
|
||||
rewrite -> (fold_unfold_loop_O (S y)).
|
||||
reflexivity.
|
||||
- intro y.
|
||||
rewrite -> (fold_unfold_loop_S x' y).
|
||||
rewrite -> (fold_unfold_loop_S (S x') y).
|
||||
exact (IHx' (S y)). }
|
||||
rewrite -> (helpful n2 n3).
|
||||
reflexivity.
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
Definition power (x n : nat) : nat :=
|
||||
let fix loop i a :=
|
||||
match i with
|
||||
O =>
|
||||
a
|
||||
| S i' =>
|
||||
loop i' (x * a)
|
||||
end
|
||||
in loop n 1.
|
||||
|
||||
Proposition about_exponentiating_with_a_sum :
|
||||
forall x n1 n2 : nat,
|
||||
power x (n1 + n2) = power x n1 * power x n2.
|
||||
Proof.
|
||||
unfold power.
|
||||
intro x.
|
||||
remember (fix loop (i a : nat) {struct i} : nat := match i with
|
||||
| 0 => a
|
||||
| S i' => loop i' (x * a)
|
||||
end)
|
||||
as loop eqn:H_loop.
|
||||
assert (fold_unfold_loop_O :
|
||||
forall a : nat,
|
||||
loop 0 a = a).
|
||||
{ intro a.
|
||||
rewrite -> H_loop.
|
||||
reflexivity. }
|
||||
assert (fold_unfold_loop_S :
|
||||
forall i' a : nat,
|
||||
loop (S i') a = loop i' (x * a)).
|
||||
{ intros n' a.
|
||||
rewrite -> H_loop.
|
||||
reflexivity. }
|
||||
assert (eureka :
|
||||
forall n a : nat,
|
||||
loop n a = loop n 1 * a).
|
||||
{ intro n.
|
||||
induction n as [ | n' IHn'].
|
||||
- intro a.
|
||||
rewrite -> (fold_unfold_loop_O a).
|
||||
rewrite -> (fold_unfold_loop_O 1).
|
||||
symmetry.
|
||||
exact (Nat.mul_1_l a).
|
||||
- intro a.
|
||||
rewrite -> (fold_unfold_loop_S n' a).
|
||||
rewrite -> (fold_unfold_loop_S n' 1).
|
||||
rewrite -> (Nat.mul_1_r x).
|
||||
rewrite -> (IHn' (x * a)).
|
||||
rewrite -> (IHn' x).
|
||||
Check (Nat.mul_assoc (loop n' 1) x a).
|
||||
exact (Nat.mul_assoc (loop n' 1) x a). }
|
||||
intro n1.
|
||||
induction n1 as [ | n1' IHn1'].
|
||||
- intro n2.
|
||||
rewrite -> (Nat.add_0_l n2).
|
||||
rewrite -> (fold_unfold_loop_O 1).
|
||||
symmetry.
|
||||
exact (Nat.mul_1_l (loop n2 1)).
|
||||
- intro n2.
|
||||
Check plus_Sn_m.
|
||||
rewrite -> (plus_Sn_m n1' n2).
|
||||
rewrite -> (fold_unfold_loop_S (n1' + n2) 1).
|
||||
rewrite -> (Nat.mul_1_r x).
|
||||
rewrite -> (fold_unfold_loop_S n1' 1).
|
||||
rewrite -> (Nat.mul_1_r x).
|
||||
rewrite -> (eureka (n1' + n2) x).
|
||||
rewrite -> (eureka n1' x).
|
||||
rewrite -> (IHn1' n2).
|
||||
Check Nat.mul_assoc.
|
||||
rewrite -> (Nat.mul_comm (loop n1' 1 * loop n2 1)).
|
||||
rewrite -> (Nat.mul_comm (loop n1' 1) x).
|
||||
Check Nat.mul_assoc.
|
||||
exact (Nat.mul_assoc x (loop n1' 1) (loop n2 1)).
|
||||
Qed.
|
||||
|
||||
(* ********** *)
|
||||
|
||||
(* end of week-05_reasoning-about-lambda-dropped-functions.v *)
|
||||
Loading…
Reference in New Issue
Block a user