Skip to content

Instantly share code, notes, and snippets.

@Iainmon
Last active September 24, 2024 18:55
Show Gist options
  • Save Iainmon/c212f5daa85487fafe4174dc229b8c82 to your computer and use it in GitHub Desktop.
Save Iainmon/c212f5daa85487fafe4174dc229b8c82 to your computer and use it in GitHub Desktop.
Lemma my_eq_sym: forall a b : Set, a = b -> b = a.
Proof.
intros a b.
intros H.
rewrite -> H || rewrite <- H.
reflexivity.
Qed.
Ltac inv H := inversion H; clear H; try subst.
Inductive expr : Set :=
| EInt : nat -> expr
| EAdd : expr -> expr -> expr
| EMul : expr -> expr -> expr.
Inductive eval : expr -> nat -> Prop :=
| eval_int : forall n, eval (EInt n) n
| eval_add : forall e e' n m,
eval e n ->
eval e' m ->
eval (EAdd e e') (n + m)
| eval_mul : forall e e' n m,
eval e n ->
eval e' m ->
eval (EMul e e') (n * m).
Fixpoint sem (e : expr) : nat :=
match e with
| EInt n => n
| EAdd n m => sem n + sem m
| EMul n m => sem n * sem m
end.
Notation "[[ x ]]" := (sem x).
Compute [[ EInt 2 ]].
Theorem sem_correct:
forall e n,
eval e n <-> [[ e ]] = n.
Proof.
intros e n.
split.
- intros Heval.
induction Heval.
+ reflexivity.
+ simpl. rewrite IHHeval1. rewrite IHHeval2. reflexivity.
+ simpl. rewrite IHHeval1. rewrite IHHeval2. reflexivity.
- intros Hsem.
generalize dependent n.
induction e.
+ intros n' Hsem. simpl in Hsem. rewrite Hsem. apply eval_int.
+ intros n' Hsem. simpl in Hsem. rewrite <- Hsem. apply eval_add.
* apply IHe1. reflexivity.
* apply IHe2. reflexivity.
+ intros n' Hsem. simpl in Hsem. rewrite <- Hsem. apply eval_mul.
* apply IHe1. reflexivity.
* apply IHe2. reflexivity.
Qed.
Theorem eval_deterministic:
forall e a b,
eval e a ->
eval e b ->
a = b.
Proof.
intros e a b.
intros Heval1 Heval2.
apply sem_correct in Heval1.
apply sem_correct in Heval2.
rewrite Heval1 in Heval2.
assumption.
Qed.
Theorem sem_eval:
forall e, eval e [[ e ]].
Proof.
intros e.
pose proof (sem_correct e [[ e ]]) as H.
apply H.
reflexivity.
Qed.
Inductive sem_eq: expr -> expr -> Prop :=
| sem_eval_eq : forall e1 e2,
[[ e1 ]] = [[ e2 ]] -> sem_eq e1 e2.
Lemma sem_eq_corollary_1:
forall e1 e2,
sem_eq e1 e2 ->
forall n,
eval e1 n <->
eval e2 n.
Proof.
intros e1 e2.
intros H1.
inversion H1.
subst.
pose proof H as H3.
remember [[ e1 ]] as m in H3.
apply eq_sym in H3.
apply eq_sym in Heqm.
intros n.
split.
-
intros H4.
apply sem_correct in H4.
rewrite Heqm in H4.
apply sem_correct.
rewrite H3.
assumption.
-
intros H4.
apply sem_correct in Heqm.
rewrite <- H3 in Heqm.
apply sem_correct in H4.
rewrite <- H4.
assumption.
Qed.
Lemma sem_eq_corollary_2:
forall e1 e2,
(forall n, eval e1 n <-> eval e2 n) ->
[[ e1 ]] = [[ e2 ]].
Proof.
intros e1 e2.
intros H1.
pose proof (sem_correct e1 [[ e2 ]]) as H2.
pose proof (sem_correct e2 [[ e1 ]]) as H3.
pose proof (H1 [[ e1 ]]) as H4.
pose proof (sem_eval e1) as H5.
apply H4 in H5.
apply H3 in H5.
apply eq_sym.
assumption.
Qed.
Lemma sem_eq_corollary_3:
forall e1 e2,
sem_eq e1 e2 <-> [[ e1 ]] = [[ e2 ]].
Proof.
intros e1 e2.
split.
- intros H1.
inversion H1.
assumption.
- intros H1.
apply sem_eval_eq.
assumption.
Qed.
Lemma sem_eq_corollary_4:
forall e1 e2,
(forall n, eval e1 n <-> eval e2 n) <->
[[ e1 ]] = [[ e2 ]].
Proof.
intros e1 e2.
split.
- intros H1.
apply sem_eq_corollary_2.
assumption.
- intros H1.
apply sem_eq_corollary_1.
apply sem_eval_eq.
assumption.
Qed.
Theorem semantic_equivalence:
forall e1 e2,
(sem_eq e1 e2 <-> [[ e1 ]] = [[ e2 ]]) /\
([[ e1 ]] = [[ e2 ]] <-> forall n, eval e1 n <-> eval e2 n) /\
((forall n, eval e1 n <-> eval e2 n) <-> sem_eq e1 e2).
Proof.
intros e1 e2.
split.
- apply sem_eq_corollary_3.
- split.
+ split.
* apply sem_eq_corollary_4.
* apply sem_eq_corollary_2.
+ split.
* intros H1.
apply sem_eval_eq.
apply sem_eq_corollary_2.
assumption.
* apply sem_eq_corollary_1.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment