proposition: Lemma expr_leq_correct_dep l: forall n m (x: expr n m) p q (y: expr p q), forall Hnp: n=p, forall Hmq: m=q, expr_leq x y = true -> e_level x + e_level y ≪ l -> cast Hnp Hmq x <==_[l] y.
proof: Proof. unfold expr_leq. apply powerfix_invariant. 2: discriminate. intros leq IH n m x p q y Hnp Hmq H Hl. destruct x; simpl e_level in Hl; repeat match goal with [ H : ?m = ?n |- _ ] => rewrite H in *; clear H end. - rewrite cast_eq. lattice. - destruct y; simpl e_level in Hl; try discriminate H. + now rewrite cast_eq. + apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + subst. rewrite cast_eq. lattice. + now rewrite cast_eq. + subst. apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite <-itr_ext. apply IH. assumption. solve_lower'. + rewrite cast_eq. apply str_refl. + subst. rewrite cast_eq. apply ldv_spec. rewrite dotx1. apply (IH _ _ _ _ _ _ eq_refl eq_refl H); solve_lower'. + subst. rewrite cast_eq. apply rdv_spec. rewrite dot1x. apply (IH _ _ _ _ _ _ eq_refl eq_refl H); solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst; try (apply landb_spec in H as [H1 H2]; apply leq_cupx; [ apply (IH _ _ _ _ _ _ eq_refl eq_refl H1); solve_lower' | apply (IH _ _ _ _ _ _ eq_refl eq_refl H2); solve_lower' ]). lattice. - destruct y; simpl e_level in Hl; try discriminate H; try subst; try (rewrite cast_eq; apply leq_capx; apply lorb_spec in H as [H|H]; (apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; [auto |solve_lower'])). lattice. rewrite cast_eq. apply landb_spec in H as [H1 H2]. apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H1; [|solve_lower']. apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H2; [|solve_lower']. hlattice. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply neg_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H). solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply landb_spec in H as [H' H]. apply landb_spec in H as [H1 H2]. revert H'. case eqb_spec. 2: discriminate. intros ? _. subst. apply dot_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H1); solve_lower'. apply (IH _ _ _ _ _ _ eq_refl eq_refl H2); solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + subst. apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply itr_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H); solve_lower'. + rewrite cast_eq. rewrite itr_str_l, <-(str_cons y). apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H. 2: solve_lower'. simpl cast in H. now rewrite H. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + subst. apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply str_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H); solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply cnv_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H); solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply landb_spec in H as [H' H]. apply landb_spec in H as [H1 H2]. revert H'. case eqb_spec. 2: discriminate. intros ? _. subst. apply ldv_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H1); solve_lower'. apply (IH _ _ _ _ _ _ eq_refl eq_refl H2); solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; try subst. + lattice. + apply leq_xcup. apply lorb_spec in H as [H|H]; apply (IH _ _ _ _ _ _ eq_refl eq_refl) in H; auto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + rewrite cast_eq. apply landb_spec in H as [H' H]. apply landb_spec in H as [H1 H2]. revert H'. case eqb_spec. 2: discriminate. intros ? _. subst. apply rdv_leq. apply (IH _ _ _ _ _ _ eq_refl eq_refl H1); solve_lower'. apply (IH _ _ _ _ _ _ eq_refl eq_refl H2); solve_lower'. - destruct y; simpl e_level in Hl; try discriminate H; subst. + lattice. + apply leq_xcup. apply lorb_spec in H as [H|H]; eapply IH in H; eauto; solve_lower'. + apply landb_spec in H as [H1 H2]. apply leq_xcap; apply IH; trivial; solve_lower'. + apply eqb_eq in H. subst. now rewrite cast_eq. Qed.
imports: kleene syntax powerfix