proposition: Lemma get_not_le_interp : forall (l:_lit) (f:Atom.hatom -> Atom.hatom -> C.t), (forall xa, t_form.[Lit.blit l] = Form.Fatom xa -> forall a b, t_atom.[xa] = Atom.Abop Atom.BO_Zle a b -> negb (Lit.is_pos l) -> rho (Lit.blit l) = Atom.interp_bool t_i (Atom.apply_binop t_i Typ.TZ Typ.TZ Typ.Tbool Zle_bool (hinterp a) (hinterp b)) -> Typ.eqb (get_type t_i t_func t_atom a) Typ.TZ -> Typ.eqb (get_type t_i t_func t_atom b) Typ.TZ -> C.interp rho (f a b)) -> C.interp rho (get_not_le l f).
proof: Proof. intros l f Hf;unfold get_not_le. destruct (Lit.is_pos l); case_eq (t_form.[Lit.blit l]);trivial;intros; try(case_eq (t_atom.[i]);trivial;intros); try (apply valid_C_true; trivial). destruct b; try (apply valid_C_true; trivial). generalize wt_t_atom;unfold Atom.wt;unfold is_true; rewrite aforallbi_spec;intros. assert (i <? length t_atom). apply PArray.get_not_default_lt. rewrite H0, def_t_atom;discriminate. apply H1 in H2;clear H1;rewrite H0 in H2;simpl in H2. rewrite !andb_true_iff in H2;decompose [and] H2;clear H2. simpl; apply Hf with (2:= H0);trivial. auto with smtcoq_core. rewrite wf_interp_form, H;simpl. unfold Atom.interp_form_hatom, Atom.interp_hatom at 1;simpl. rewrite Atom.t_interp_wf, H0;simpl;trivial. trivial. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz