Library synEq
Require Import language.
Fixpoint HSynEq (E1 E2: HExpr) : bool :=
match E1, E2 with
| HvarExpr v, HvarExpr v' => beq_SkalVar (HSkalVar v) (HSkalVar v')
| HemptyExpr, HemptyExpr => true
| HupdateExpr h a a2, HupdateExpr h' a' a2' => andb (HSynEq h h') (andb (ASynEq a a')
(ASynEq a2 a2'))
| _, _ => false
end
with
ASynEq (E1 E2: AExpr) : bool :=
match E1, E2 with
| SvarExpr v, SvarExpr v' => beq_SkalVar (ASkalVar v) (ASkalVar v')
| IntExpr i, IntExpr i' => if Z_eq_dec i i' then true else false
| AopExpr E1 op E2, AopExpr E1' op' E2' =>
andb (andb (if AOp_Eq op op' then true else false) (ASynEq E1 E1')) (ASynEq E2 E2')
| ArrayAccess h a, ArrayAccess h' a' => andb (HSynEq h h') (ASynEq a a')
| _, _=> false end.
Fixpoint BSynEq(E1 E2 : BExpr): bool :=
match E1, E2 with
| BvalExpr v, BvalExpr v' => Bool.eqb v v'
| BvarExpr v, BvarExpr v' => beq_SkalVar (BSkalVar v) (BSkalVar v')
| BopExpr E1 op E2, BopExpr E1' op' E2' =>
andb (andb (if BOp_Eq op op' then true else false) (ASynEq E1 E1')) (ASynEq E2 E2')
| AndExpr E1 E2, AndExpr E1' E2' => andb (BSynEq E1 E1') (BSynEq E2 E2')
| OrExpr E1 E2, OrExpr E1' E2' => andb (BSynEq E1 E1') (BSynEq E2 E2')
| NotExpr E, NotExpr E' => (BSynEq E E')
| _,_ => false end.
Fixpoint synEq(E1 E2 : Expr): bool :=
match E1, E2 with
| AExp e, AExp e2 => ASynEq e e2
| BExp e, BExp e2 => BSynEq e e2
| HExp e, HExp e2 => HSynEq e e2
| _,_ => false
end.
Theorem beq_SkalVar_eq : forall x y, beq_SkalVar x y =true -> x = y.
intros. destruct x. destruct y. unfold beq_SkalVar in H. destruct a. destruct a0.
apply Zeq_bool_eq in H. subst. auto. unfold beq_SkalVar in H. destruct a. inversion H.
destruct a. destruct h. inv H. destruct b. destruct y. destruct a. inv H.
destruct b. apply Zeq_bool_eq in H. subst; auto. destruct h; inv H.
destruct h; destruct y. destruct a; inv H. destruct b; inv H.
destruct h. apply Zeq_bool_eq in H. subst. auto.
Qed.
Theorem beq_eq_SkalVar : forall x y, x=y -> beq_SkalVar x y =true.
intros. subst. destruct y. unfold beq_SkalVar. destruct a. destruct (Zeq_is_eq_bool z z). apply H. auto.
unfold beq_SkalVar. destruct b. rewrite <- Zeq_is_eq_bool. auto.
destruct h. unfold beq_SkalVar. rewrite <- Zeq_is_eq_bool. auto.
Qed.
Theorem beq_SkalVar_sem: forall x y, beq_SkalVar x y = beq_SkalVar y x.
intros. unfold beq_SkalVar in *. destruct x. destruct y. destruct a0. destruct a.
remember (Zeq_bool z z0). destruct b. symmetry in Heqb.
rewrite <- Zeq_is_eq_bool in *. auto. symmetry in Heqb. apply Zeq_bool_neq in Heqb.
unfold not in Heqb. unfold Zeq_bool. remember (z0 ?= z)%Z. destruct c; auto.
symmetry in Heqc. rewrite Zcompare_Eq_iff_eq in Heqc. subst. intuition.
destruct a. destruct b. auto. destruct a. destruct h. auto. destruct b.
destruct y; auto. destruct a; auto. destruct b.
remember (Zeq_bool z0 z). destruct b. symmetry in Heqb.
rewrite <- Zeq_is_eq_bool in *. auto. symmetry in Heqb. apply Zeq_bool_neq in Heqb.
unfold not in Heqb. unfold Zeq_bool. remember (z ?= z0)%Z. destruct c; auto.
symmetry in Heqc. rewrite Zcompare_Eq_iff_eq in Heqc. subst. intuition.
destruct h. auto. destruct h. destruct y. destruct a. auto. destruct b. auto.
destruct h.
remember (Zeq_bool z0 z). destruct b. symmetry in Heqb.
rewrite <- Zeq_is_eq_bool in *. auto.
symmetry in Heqb. apply Zeq_bool_neq in Heqb.
unfold not in Heqb. unfold Zeq_bool. remember (z ?= z0)%Z. destruct c; auto.
symmetry in Heqc. rewrite Zcompare_Eq_iff_eq in Heqc. subst. intuition.
Qed.
Hint Resolve beq_SkalVar_eq.
Hint Resolve beq_eq_SkalVar.
Lemma beq_SkalVar_refl : forall x, beq_SkalVar x x = true.
Proof.
intros. auto. Qed.
Hint Resolve beq_SkalVar_refl.
Theorem bneq_Skalvar_neq: forall x y, false = beq_SkalVar x y -> x <> y.
intros. unfold not. intros. subst. rewrite beq_SkalVar_refl in H. inv H.
Qed.
Hint Resolve bneq_Skalvar_neq.
Lemma hSynEq_eq: forall a b, true = HSynEq a b -> a = b.
intros a. induction a using HExpr_ind_mut with
(P0:= fun x => forall y, true=ASynEq x y -> x=y); intros. simpl in H. destruct b; inv H.
symmetry in H1. apply beq_SkalVar_eq in H1. inv H1. auto. destruct b; inv H.
auto. simpl in H. destruct b; inv H. symmetry in H1. apply andb_true_iff in H1.
destruct H1. symmetry in H. apply andb_true_iff in H0. destruct H0. erewrite IHa; eauto.
erewrite IHa1; eauto. erewrite IHa0; eauto. simpl in *. destruct y.
symmetry in H. apply beq_SkalVar_eq in H. inv H. auto. inv H. inv H.
inv H. simpl in H. destruct y; inv H. remember (Z_eq_dec a a0). destruct s.
subst. auto. inv H1. destruct y; inv H. remember (AOp_Eq a0 a2). destruct b; inv H1.
symmetry in H0. apply andb_true_iff in H0. destruct H0. erewrite IHa; eauto.
erewrite IHa0; eauto. symmetry in Heqb. apply AOp_Eq_Eq in Heqb. subst; auto.
simpl in *. destruct y; inv H. symmetry in H1. apply andb_true_iff in H1.
destruct H1. erewrite IHa0; eauto. erewrite IHa; eauto.
Qed.
Lemma aSynEq_eq: forall a b, true = ASynEq a b -> a = b.
intros a. induction a using AExpr_ind_mut with
(P:= fun x => forall y, true=HSynEq x y -> x=y); intros. destruct y; inv H.
symmetry in H1. apply beq_SkalVar_eq in H1.
inv H1. auto. destruct y; inv H. auto.
destruct y; inv H. symmetry in H1. apply andb_true_iff in H1. destruct H1.
apply andb_true_iff in H0. destruct H0. erewrite IHa1; eauto.
erewrite IHa2; eauto. erewrite IHa3; eauto. destruct b; inv H.
symmetry in H1. apply beq_SkalVar_eq in H1. inv H1. auto.
destruct b; inv H. remember (Z_eq_dec a a0). destruct s.
subst; auto. inv H1.
destruct b; inv H. remember (AOp_Eq a2 a). destruct b.
symmetry in Heqb. apply AOp_Eq_Eq in Heqb. subst. auto.
symmetry in H1. apply andb_true_iff in H1. destruct H1.
apply andb_true_iff in H. destruct H. subst.
erewrite IHa1; eauto.
erewrite IHa2; eauto.
inv H1.
destruct b; inv H. symmetry in H1. apply andb_true_iff in H1.
destruct H1. erewrite IHa; eauto. erewrite IHa0; eauto.
Qed.
Lemma bSynEq_eq: forall a c, true = BSynEq a c -> a = c.
intros a. induction a; intros; destruct c; inv H. symmetry in H1.
apply beq_SkalVar_eq in H1. inv H1. auto. unfold eqb in H1.
destruct b0. destruct b. auto. inv H1. destruct b. inv H1. auto.
symmetry in H1. rewrite andb_true_iff in H1.
destruct H1. rewrite andb_true_iff in H. destruct H. rewrite (aSynEq_eq a a1).
rewrite (aSynEq_eq a0 a2). remember (BOp_Eq b b0). destruct b1. symmetry in Heqb1.
apply BOp_Eq_Eq in Heqb1.
subst. auto. inv H.
symmetry in H0. auto. symmetry in H1. auto.
symmetry in H1. rewrite andb_true_iff in H1. destruct H1.
rewrite (IHa1 c1). rewrite (IHa2 c2). auto.
auto. auto.
symmetry in H1. rewrite andb_true_iff in H1. destruct H1.
rewrite (IHa1 c1). rewrite (IHa2 c2). auto.
auto. auto.
rewrite (IHa c). auto. auto.
Qed.
Lemma synEq_eq : forall a c, true = synEq a c -> a = c.
Proof.
intros.
destruct a; destruct c; inv H. apply aSynEq_eq in H1. subst. auto.
apply bSynEq_eq in H1. subst. auto.
apply hSynEq_eq in H1; subst; auto.
Qed.
Lemma eqb_refl: forall b, eqb b b= true.
intros. destruct b; auto.
Qed.
Lemma hSynEq_refl: forall h, HSynEq h h = true.
intros. induction h using HExpr_ind_mut with
(P0:= fun l => ASynEq l l = true).
simpl. apply beq_SkalVar_refl. auto.
simpl. apply andb_true_iff. split. auto. apply andb_true_iff. split; auto.
simpl. apply beq_SkalVar_refl. simpl. remember (Z_eq_dec a a). destruct s; auto.
simpl. remember (AOp_Eq a0 a0). destruct b. intuition. destruct a0; inv Heqb.
simpl. intuition.
Qed.
Lemma aSynEq_refl: forall a, ASynEq a a = true.
Proof.
intros. induction a using AExpr_ind_mut with
(P:= fun l => HSynEq l l = true); try (apply beq_SkalVar_refl); auto.
simpl. apply andb_true_iff; split;try( apply andb_true_iff; split); auto.
simpl. remember (Z_eq_dec a a). destruct s; auto.
simpl. destruct a2; simpl; intuition.
simpl. apply andb_true_iff. split; auto.
Qed.
Lemma bSynEq_refl: forall b, BSynEq b b = true.
intros. induction b; auto. destruct b. simpl. apply beq_SkalVar_refl.
simpl. apply eqb_refl. simpl. repeat rewrite aSynEq_refl. destruct b; intuition.
simpl. rewrite IHb1. rewrite IHb2. auto.
simpl. rewrite IHb1. rewrite IHb2. auto.
Qed.
Fixpoint HSynEq (E1 E2: HExpr) : bool :=
match E1, E2 with
| HvarExpr v, HvarExpr v' => beq_SkalVar (HSkalVar v) (HSkalVar v')
| HemptyExpr, HemptyExpr => true
| HupdateExpr h a a2, HupdateExpr h' a' a2' => andb (HSynEq h h') (andb (ASynEq a a')
(ASynEq a2 a2'))
| _, _ => false
end
with
ASynEq (E1 E2: AExpr) : bool :=
match E1, E2 with
| SvarExpr v, SvarExpr v' => beq_SkalVar (ASkalVar v) (ASkalVar v')
| IntExpr i, IntExpr i' => if Z_eq_dec i i' then true else false
| AopExpr E1 op E2, AopExpr E1' op' E2' =>
andb (andb (if AOp_Eq op op' then true else false) (ASynEq E1 E1')) (ASynEq E2 E2')
| ArrayAccess h a, ArrayAccess h' a' => andb (HSynEq h h') (ASynEq a a')
| _, _=> false end.
Fixpoint BSynEq(E1 E2 : BExpr): bool :=
match E1, E2 with
| BvalExpr v, BvalExpr v' => Bool.eqb v v'
| BvarExpr v, BvarExpr v' => beq_SkalVar (BSkalVar v) (BSkalVar v')
| BopExpr E1 op E2, BopExpr E1' op' E2' =>
andb (andb (if BOp_Eq op op' then true else false) (ASynEq E1 E1')) (ASynEq E2 E2')
| AndExpr E1 E2, AndExpr E1' E2' => andb (BSynEq E1 E1') (BSynEq E2 E2')
| OrExpr E1 E2, OrExpr E1' E2' => andb (BSynEq E1 E1') (BSynEq E2 E2')
| NotExpr E, NotExpr E' => (BSynEq E E')
| _,_ => false end.
Fixpoint synEq(E1 E2 : Expr): bool :=
match E1, E2 with
| AExp e, AExp e2 => ASynEq e e2
| BExp e, BExp e2 => BSynEq e e2
| HExp e, HExp e2 => HSynEq e e2
| _,_ => false
end.
Theorem beq_SkalVar_eq : forall x y, beq_SkalVar x y =true -> x = y.
intros. destruct x. destruct y. unfold beq_SkalVar in H. destruct a. destruct a0.
apply Zeq_bool_eq in H. subst. auto. unfold beq_SkalVar in H. destruct a. inversion H.
destruct a. destruct h. inv H. destruct b. destruct y. destruct a. inv H.
destruct b. apply Zeq_bool_eq in H. subst; auto. destruct h; inv H.
destruct h; destruct y. destruct a; inv H. destruct b; inv H.
destruct h. apply Zeq_bool_eq in H. subst. auto.
Qed.
Theorem beq_eq_SkalVar : forall x y, x=y -> beq_SkalVar x y =true.
intros. subst. destruct y. unfold beq_SkalVar. destruct a. destruct (Zeq_is_eq_bool z z). apply H. auto.
unfold beq_SkalVar. destruct b. rewrite <- Zeq_is_eq_bool. auto.
destruct h. unfold beq_SkalVar. rewrite <- Zeq_is_eq_bool. auto.
Qed.
Theorem beq_SkalVar_sem: forall x y, beq_SkalVar x y = beq_SkalVar y x.
intros. unfold beq_SkalVar in *. destruct x. destruct y. destruct a0. destruct a.
remember (Zeq_bool z z0). destruct b. symmetry in Heqb.
rewrite <- Zeq_is_eq_bool in *. auto. symmetry in Heqb. apply Zeq_bool_neq in Heqb.
unfold not in Heqb. unfold Zeq_bool. remember (z0 ?= z)%Z. destruct c; auto.
symmetry in Heqc. rewrite Zcompare_Eq_iff_eq in Heqc. subst. intuition.
destruct a. destruct b. auto. destruct a. destruct h. auto. destruct b.
destruct y; auto. destruct a; auto. destruct b.
remember (Zeq_bool z0 z). destruct b. symmetry in Heqb.
rewrite <- Zeq_is_eq_bool in *. auto. symmetry in Heqb. apply Zeq_bool_neq in Heqb.
unfold not in Heqb. unfold Zeq_bool. remember (z ?= z0)%Z. destruct c; auto.
symmetry in Heqc. rewrite Zcompare_Eq_iff_eq in Heqc. subst. intuition.
destruct h. auto. destruct h. destruct y. destruct a. auto. destruct b. auto.
destruct h.
remember (Zeq_bool z0 z). destruct b. symmetry in Heqb.
rewrite <- Zeq_is_eq_bool in *. auto.
symmetry in Heqb. apply Zeq_bool_neq in Heqb.
unfold not in Heqb. unfold Zeq_bool. remember (z ?= z0)%Z. destruct c; auto.
symmetry in Heqc. rewrite Zcompare_Eq_iff_eq in Heqc. subst. intuition.
Qed.
Hint Resolve beq_SkalVar_eq.
Hint Resolve beq_eq_SkalVar.
Lemma beq_SkalVar_refl : forall x, beq_SkalVar x x = true.
Proof.
intros. auto. Qed.
Hint Resolve beq_SkalVar_refl.
Theorem bneq_Skalvar_neq: forall x y, false = beq_SkalVar x y -> x <> y.
intros. unfold not. intros. subst. rewrite beq_SkalVar_refl in H. inv H.
Qed.
Hint Resolve bneq_Skalvar_neq.
Lemma hSynEq_eq: forall a b, true = HSynEq a b -> a = b.
intros a. induction a using HExpr_ind_mut with
(P0:= fun x => forall y, true=ASynEq x y -> x=y); intros. simpl in H. destruct b; inv H.
symmetry in H1. apply beq_SkalVar_eq in H1. inv H1. auto. destruct b; inv H.
auto. simpl in H. destruct b; inv H. symmetry in H1. apply andb_true_iff in H1.
destruct H1. symmetry in H. apply andb_true_iff in H0. destruct H0. erewrite IHa; eauto.
erewrite IHa1; eauto. erewrite IHa0; eauto. simpl in *. destruct y.
symmetry in H. apply beq_SkalVar_eq in H. inv H. auto. inv H. inv H.
inv H. simpl in H. destruct y; inv H. remember (Z_eq_dec a a0). destruct s.
subst. auto. inv H1. destruct y; inv H. remember (AOp_Eq a0 a2). destruct b; inv H1.
symmetry in H0. apply andb_true_iff in H0. destruct H0. erewrite IHa; eauto.
erewrite IHa0; eauto. symmetry in Heqb. apply AOp_Eq_Eq in Heqb. subst; auto.
simpl in *. destruct y; inv H. symmetry in H1. apply andb_true_iff in H1.
destruct H1. erewrite IHa0; eauto. erewrite IHa; eauto.
Qed.
Lemma aSynEq_eq: forall a b, true = ASynEq a b -> a = b.
intros a. induction a using AExpr_ind_mut with
(P:= fun x => forall y, true=HSynEq x y -> x=y); intros. destruct y; inv H.
symmetry in H1. apply beq_SkalVar_eq in H1.
inv H1. auto. destruct y; inv H. auto.
destruct y; inv H. symmetry in H1. apply andb_true_iff in H1. destruct H1.
apply andb_true_iff in H0. destruct H0. erewrite IHa1; eauto.
erewrite IHa2; eauto. erewrite IHa3; eauto. destruct b; inv H.
symmetry in H1. apply beq_SkalVar_eq in H1. inv H1. auto.
destruct b; inv H. remember (Z_eq_dec a a0). destruct s.
subst; auto. inv H1.
destruct b; inv H. remember (AOp_Eq a2 a). destruct b.
symmetry in Heqb. apply AOp_Eq_Eq in Heqb. subst. auto.
symmetry in H1. apply andb_true_iff in H1. destruct H1.
apply andb_true_iff in H. destruct H. subst.
erewrite IHa1; eauto.
erewrite IHa2; eauto.
inv H1.
destruct b; inv H. symmetry in H1. apply andb_true_iff in H1.
destruct H1. erewrite IHa; eauto. erewrite IHa0; eauto.
Qed.
Lemma bSynEq_eq: forall a c, true = BSynEq a c -> a = c.
intros a. induction a; intros; destruct c; inv H. symmetry in H1.
apply beq_SkalVar_eq in H1. inv H1. auto. unfold eqb in H1.
destruct b0. destruct b. auto. inv H1. destruct b. inv H1. auto.
symmetry in H1. rewrite andb_true_iff in H1.
destruct H1. rewrite andb_true_iff in H. destruct H. rewrite (aSynEq_eq a a1).
rewrite (aSynEq_eq a0 a2). remember (BOp_Eq b b0). destruct b1. symmetry in Heqb1.
apply BOp_Eq_Eq in Heqb1.
subst. auto. inv H.
symmetry in H0. auto. symmetry in H1. auto.
symmetry in H1. rewrite andb_true_iff in H1. destruct H1.
rewrite (IHa1 c1). rewrite (IHa2 c2). auto.
auto. auto.
symmetry in H1. rewrite andb_true_iff in H1. destruct H1.
rewrite (IHa1 c1). rewrite (IHa2 c2). auto.
auto. auto.
rewrite (IHa c). auto. auto.
Qed.
Lemma synEq_eq : forall a c, true = synEq a c -> a = c.
Proof.
intros.
destruct a; destruct c; inv H. apply aSynEq_eq in H1. subst. auto.
apply bSynEq_eq in H1. subst. auto.
apply hSynEq_eq in H1; subst; auto.
Qed.
Lemma eqb_refl: forall b, eqb b b= true.
intros. destruct b; auto.
Qed.
Lemma hSynEq_refl: forall h, HSynEq h h = true.
intros. induction h using HExpr_ind_mut with
(P0:= fun l => ASynEq l l = true).
simpl. apply beq_SkalVar_refl. auto.
simpl. apply andb_true_iff. split. auto. apply andb_true_iff. split; auto.
simpl. apply beq_SkalVar_refl. simpl. remember (Z_eq_dec a a). destruct s; auto.
simpl. remember (AOp_Eq a0 a0). destruct b. intuition. destruct a0; inv Heqb.
simpl. intuition.
Qed.
Lemma aSynEq_refl: forall a, ASynEq a a = true.
Proof.
intros. induction a using AExpr_ind_mut with
(P:= fun l => HSynEq l l = true); try (apply beq_SkalVar_refl); auto.
simpl. apply andb_true_iff; split;try( apply andb_true_iff; split); auto.
simpl. remember (Z_eq_dec a a). destruct s; auto.
simpl. destruct a2; simpl; intuition.
simpl. apply andb_true_iff. split; auto.
Qed.
Lemma bSynEq_refl: forall b, BSynEq b b = true.
intros. induction b; auto. destruct b. simpl. apply beq_SkalVar_refl.
simpl. apply eqb_refl. simpl. repeat rewrite aSynEq_refl. destruct b; intuition.
simpl. rewrite IHb1. rewrite IHb2. auto.
simpl. rewrite IHb1. rewrite IHb2. auto.
Qed.