proposition: Lemma valid_check_congr : forall leq eqs, C.interp rho (check_congr leq eqs).
proof: Proof. unfold check_congr;intros leq eqs;apply get_eq_interp;intros. case_eq (t_atom .[ a]);intros;auto with smtcoq_euf smtcoq_core; case_eq (t_atom .[ b]);intros;auto with smtcoq_euf smtcoq_core. destruct (Atom.reflect_uop_eqb u u0);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl. rewrite HHb, HHa. simpl. rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). inversion H6;subst. unfold Atom.interp_hatom in H10. rewrite <- HHa; rewrite <- HHb, H10;trivial with smtcoq_euf smtcoq_core. inversion H7. apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. destruct (Atom.reflect_bop_eqb b0 b1);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop. unfold Atom.interp_hatom;simpl. rewrite HHb, HHa;simpl. rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). inversion H6;clear H6;subst. inversion H12;clear H12;subst. unfold Atom.interp_hatom in H10, H8. rewrite <- HHa. rewrite <- HHb, H10, H8;trivial with smtcoq_euf smtcoq_core. inversion H7. apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. destruct (Misc.reflect_eqb i i0);[subst | auto with smtcoq_euf smtcoq_core]. apply build_congr_correct;intros. simpl;rewrite Lit.interp_lit, orb_false_r;unfold Var.interp. rewrite H1. generalize (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom a), (Atom.check_aux_interp_hatom _ t_func _ wf_t_atom b). rewrite Typ.eqb_spec in H2. rewrite Typ.eqb_spec in H3. unfold Atom.get_type in H2, H3. rewrite H2,H3. intros [va HHa] [vb HHb]. unfold Atom.apply_binop;unfold Atom.interp_hatom;simpl. rewrite HHb, HHa;simpl. rewrite Atom.t_interp_wf in HHa; auto with smtcoq_euf smtcoq_core. rewrite H4 in HHa. simpl in HHa. rewrite Atom.t_interp_wf in HHb; auto with smtcoq_euf smtcoq_core. rewrite H5 in HHb. simpl in HHb. rewrite Typ.cast_refl;simpl. assert (Atom.Bval t_i t va = Atom.Bval t_i t vb). rewrite <- HHa;rewrite <- HHb;destruct (t_func.[i0]). apply f_equal;clear HHa HHb va vb H5 H4. induction H6;simpl;trivial with smtcoq_euf smtcoq_core. unfold Atom.interp_hatom in H4. rewrite IHForall2, H4;trivial with smtcoq_euf smtcoq_core. inversion H7. apply Eqdep_dec.inj_pair2_eq_dec in H9;trivial with smtcoq_euf smtcoq_core. rewrite H9. apply Typ.i_eqb_refl. intros x y;destruct (Typ.reflect_eqb x y);auto with smtcoq_euf smtcoq_core. Qed.
imports: Bool List Int63 PArray State SMT_terms