A Hugo incarnation of the blog. https://danilafe.com
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
 
 
 
 
 
 

179 lines
6.5 KiB

Require Import Coq.Lists.List.
From Ltac2 Require Import Ltac2.
Inductive intrinsic :=
| swap
| clone
| drop
| quote
| compose
| apply.
Inductive expr :=
| e_int (i : intrinsic)
| e_quote (e : expr)
| e_comp (e1 e2 : expr).
Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e.
Inductive IsValue : expr -> Prop :=
| Val_quote : forall {e : expr}, IsValue (e_quote e).
Definition value := { v : expr & IsValue v }.
Definition value_stack := list value.
Definition v_quote (e : expr) := existT IsValue (e_quote e) Val_quote.
Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop :=
| Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)
| Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs)
| Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs
| Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (projT1 v)) :: vs)
| Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs)
| Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs'
with Sem_expr : value_stack -> expr -> value_stack -> Prop :=
| Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs'
| Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs)
| Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack),
Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3.
Definition false : expr := e_quote (e_int drop).
Definition false_v : value := v_quote (e_int drop).
Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)).
Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)).
Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs).
Proof.
intros v v' vs.
eapply Sem_e_comp.
- apply Sem_e_quote.
- apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop.
Qed.
Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs).
Proof.
intros v v' vs.
eapply Sem_e_comp.
- apply Sem_e_quote.
- apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp.
* apply Sem_e_int. apply Sem_swap.
* apply Sem_e_int. apply Sem_drop.
Qed.
Definition or : expr := e_comp (e_int clone) (e_int apply).
Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs).
Proof with apply Sem_e_int.
intros v vs.
eapply Sem_e_comp...
- apply Sem_clone.
- apply Sem_apply... apply Sem_drop.
Qed.
Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs).
Proof with apply Sem_e_int.
intros v vs.
eapply Sem_e_comp...
- apply Sem_clone...
- apply Sem_apply. eapply Sem_e_comp...
* apply Sem_swap.
* apply Sem_drop.
Qed.
Definition or_false_false := or_false_v false_v.
Definition or_false_true := or_false_v true_v.
Definition or_true_false := or_true false_v.
Definition or_true_true := or_true true_v.
Fixpoint quote_n (n : nat) :=
match n with
| O => e_int quote
| S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil)
end.
Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
Proof with apply Sem_e_int.
intros v1 v2 vs. simpl.
repeat (eapply Sem_e_comp)...
- apply Sem_quote.
- apply Sem_swap.
- apply Sem_quote.
- apply Sem_swap.
- apply Sem_compose.
Qed.
Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
Proof with apply Sem_e_int.
intros v1 v2 v3 vs. simpl.
repeat (eapply Sem_e_comp)...
- apply Sem_quote.
- apply Sem_swap.
- apply Sem_quote.
- apply Sem_swap.
- apply Sem_compose.
- apply Sem_swap.
- apply Sem_quote.
- apply Sem_swap.
- apply Sem_compose.
Qed.
Ltac2 rec solve_basic () := Control.enter (fun _ =>
match! goal with
| [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap
| [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone
| [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop
| [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote
| [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose
| [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
| [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
| [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
| [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
| [_ : _ |- _] => ()
end).
Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
Proof. intros. simpl. solve_basic (). Qed.
Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack),
Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
Proof. intros. simpl. solve_basic (). Qed.
Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil).
Lemma eval_value : forall (v : value) (vs : value_stack),
Sem_expr vs (projT1 v) (v :: vs).
Proof.
intros v vs.
destruct v. destruct i.
simpl. apply Sem_e_quote.
Qed.
Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs).
Proof.
intros. unfold rotate_n. simpl. solve_basic ().
repeat (eapply Sem_e_comp); apply eval_value.
Qed.
Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack),
Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs).
Proof.
intros. unfold rotate_n. simpl. solve_basic ().
repeat (eapply Sem_e_comp); apply eval_value.
Qed.
Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack),
Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'.
Proof.
intros e1 e2 e3 vs vs'.
split; intros Heval.
- inversion Heval; subst. inversion H4; subst.
eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6.
- inversion Heval; subst. inversion H2; subst.
eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4.
Qed.