proposition: Lemma algebraic_monotonicity_criterion : appMonCond -> absMonCond -> algebraic_monotonicity.
proof: Proof. intros CApp CAbs T; revert CApp CAbs. apply well_founded_ind with (R := subterm) (P := fun T => appMonCond -> absMonCond -> forall (pos: Pos T) (Mpos Npos: PlaceHolder pos) (M := proj1_sig2 Mpos) (N := proj1_sig2 Npos), algebraic T -> algebraic M -> algebraic N -> ~isFunApp (T // pos) -> M -R-> N -> swap Mpos -R-> swap Npos). apply subterm_wf. clear T; intros T IH CApp CAbs pos Mpos Npos M N Talg Malg Nalg Tpos MN. induction pos. replace (swap Mpos) with (proj1_sig2 Mpos). replace (swap Npos) with (proj1_sig2 Npos). trivial. apply term_eq; trivial. rewrite swap_env_eq; destruct Npos; try_solve. rewrite swap_term_is; try_solve. apply term_eq; trivial. rewrite swap_env_eq; destruct Mpos; try_solve. rewrite swap_term_is; try_solve. set (Labs := swap_abs Mpos). set (Rabs := swap_abs Npos). apply CAbs with Labs Rabs. apply algebraic_absBody. apply algebraic_swap; trivial. apply algebraic_absBody. apply algebraic_swap; trivial. apply type_eq_absType_eq. do 2 rewrite swap_type_eq; trivial. destruct (placeHolder_abs Mpos) as [MLpos ML]. destruct (placeHolder_abs Npos) as [NLpos NL]. replace (absBody Labs) with (swap MLpos). replace (absBody Rabs) with (swap NLpos). apply IH; trivial. change (buildT AbsB) with (@absBody (buildT (TAbs AbsB)) I). apply absBody_subterm. change (buildT AbsB) with (@absBody (buildT (TAbs AbsB)) I). apply algebraic_absBody; trivial. rewrite ML; trivial. rewrite NL; trivial. rewrite ML; rewrite NL; trivial. apply swap_in_abs; trivial. apply TAbs; trivial. apply swap_in_abs; trivial. apply TAbs; trivial. set (Lapp := swap_left_app Mpos). set (Rapp := swap_left_app Npos). apply CApp with Lapp Rapp. apply algebraic_swap; trivial. apply algebraic_swap; trivial. destruct (isFunS_dec (appHead (buildT (TApp AppL AppR)))). right; right; split. apply swap_isFunApp; trivial. destruct (algebraic_swap_funApp Mpos Npos) as [[l r] [T [TP [[PHL PHR] [Targ [Tnfa [TM [TN [MNhead [Margs Nargs]]]]]]]]]]; trivial. split; simpl in *; trivial. ex (l, r) (swap PHL) (swap PHR); repeat split; trivial. apply IH; trivial. apply arg_subterm; trivial. apply algebraic_arg with (buildT (TApp AppL AppR)); simpl; trivial. rewrite TM; trivial. rewrite TN; trivial. rewrite TM; rewrite TN; trivial. left; repeat split. apply swap_not_funApp; try_solve; fold M. inversion Malg; term_inv M. apply swap_not_funApp; try_solve; fold N. inversion Nalg; term_inv N. destruct (placeHolder_appL Mpos) as [MLpos ML]. destruct (placeHolder_appL Npos) as [NLpos NL]. replace (appBodyL Lapp) with (swap MLpos). replace (appBodyL Rapp) with (swap NLpos). apply IH; trivial. change (buildT AppL) with (@appBodyL (buildT (TApp AppL AppR)) I). apply appBodyL_subterm; trivial. change (buildT AppL) with (@appBodyL (buildT (TApp AppL AppR)) I). apply algebraic_appBodyL; trivial. rewrite ML; trivial. rewrite NL; trivial. rewrite ML; rewrite NL; trivial. apply swap_in_appL; trivial. apply swap_in_appL; trivial. apply swap_appR_eq. set (Lapp := swap_right_app Mpos). set (Rapp := swap_right_app Npos). apply CApp with Lapp Rapp. apply algebraic_swap; trivial. apply algebraic_swap; trivial. destruct (isFunS_dec (appHead (buildT (TApp AppL AppR)))). right; right; split. apply swap_isFunApp; trivial. destruct (algebraic_swap_funApp Mpos Npos) as [[l r] [T [TP [[PHL PHR] [Targ [Tnfa [TM [TN [MNhead [Margs Nargs]]]]]]]]]]; trivial. repeat split; simpl in *; trivial. ex (l, r) (swap PHL) (swap PHR); repeat split; trivial. apply IH; trivial. apply arg_subterm; trivial. apply algebraic_arg with (buildT (TApp AppL AppR)); simpl; trivial. rewrite TM; trivial. rewrite TN; trivial. rewrite TM; rewrite TN; trivial. right; left; repeat split. apply swap_not_funApp; try_solve; fold M. inversion Malg; term_inv M. apply swap_not_funApp; try_solve; fold N. inversion Nalg; term_inv N. apply swap_appL_eq. destruct (placeHolder_appR Mpos) as [MLpos ML]. destruct (placeHolder_appR Npos) as [NLpos NL]. replace (appBodyR Lapp) with (swap MLpos). replace (appBodyR Rapp) with (swap NLpos). apply IH; trivial. change (buildT AppR) with (@appBodyR (buildT (TApp AppL AppR)) I). apply appBodyR_subterm; trivial. change (buildT AppR) with (@appBodyR (buildT (TApp AppL AppR)) I). apply algebraic_appBodyR; trivial. rewrite ML; trivial. rewrite NL; trivial. rewrite ML; rewrite NL; trivial. apply swap_in_appR; trivial. apply swap_in_appR; trivial. Qed.
imports: CoLoR(RelExtras ListExtras TermsEta LogicUtil) Coq(Morphisms)