proposition: Lemma eval_ind3 (phi : U) (f1 : U1) (p1 : pred (K1*V1)) (a1 : R1 -> K1 -> V1 -> R1) (z1 : R1) (f2 : U2) (p2 : pred (K2*V2)) (a2 : R2 -> K2 -> V2 -> R2) (z2 : R2) : um_mono phi -> dom phi = dom f1 -> range phi = dom f2 -> P z1 z2 -> (forall k1 v1 k2 v2 z1 z2, (k1, k2) \In phi -> (k1, v1) \In f1 -> (k2, v2) \In f2 -> P z1 z2 -> P (if p1 (k1, v1) then a1 z1 k1 v1 else z1) (if p2 (k2, v2) then a2 z2 k2 v2 else z2)) -> P (eval a1 p1 f1 z1) (eval a2 p2 f2 z2).
proof: Proof. elim/um_indf: f1 f2 phi z1 z2 =>[||k1 v1 f1 IH W Po] f2 phi1 z1 z2 /ummonoP M1 D1 R Hz H. - rewrite eval_undef eval_dom0 // -R; move/domE: D1; rewrite dom_undef. case W1 : (valid phi1); first by move/(dom0E W1)=>->; rewrite range0. by move/negbT/invalidE: W1=>->; rewrite dom_undef range_undef. - rewrite eval0 eval_dom0 // -R; move/domE: D1; rewrite dom0. case W1 : (valid phi1); first by move/(dom0E W1)=>->; rewrite range0. by move/negbT/invalidE: W1=>->; rewrite dom_undef range_undef. have A1 : all (ord k1) (dom f1) by apply: order_path_min Po; apply: trans. case W1 : (valid phi1); last first. - by move/negbT/invalidE: W1 D1 R=>->; rewrite dom_undef domPtUnK. rewrite domPtUnK // in D1 *; rewrite evalPtUn //. have [k2 I1] : exists k2, (k1, k2) \In phi1. - by apply/In_domX; rewrite D1 inE eq_refl. have I2 : (k1, v1) \In pts k1 v1 \+ f1 by apply/InPtUnE=>//; left. have [v2 I3] : exists v2, (k2, v2) \In f2. - by apply/In_domX; rewrite -R; apply/mem_seqP/(In_range I1). move: (H _ _ _ _ _ _ I1 I2 I3 Hz)=>Hp. set phi2 := free phi1 k1. have W2 : valid f2 by move/In_dom/dom_valid: I3. have E2 : f2 = pts k2 v2 \+ free f2 k2 by apply/In_eta: I3. have A2 : all (ord k2) (dom (free f2 k2)). - apply/allP=>x; rewrite domF inE E2 domPtUn inE -E2 W2 /= domF inE. case: eqP=>//= N; rewrite -R =>R'; move/mem_seqP/In_rangeX: (R'). case=>k' H1; apply: M1 (I1) (H1) _; move/allP: A1; apply. move/In_dom: H1 (H1); rewrite D1 inE; case/orP=>//= /eqP ->. by move/(In_fun I1)/N. rewrite E2 evalPtUn -?E2 //. have M2 : um_mono phi2. - by apply/ummonoP=>???? /InF [_ _ /M1] X /InF [_ _]; apply: X. have D2 : dom phi2 = dom f1. - apply/domE=>x; rewrite domF inE D1 inE eq_sym. by case: eqP=>// ->{x}; rewrite (negbTE (validPtUnD W)). have R2' : range phi2 = dom (free f2 k2). move/In_eta: (I1) (R)=>E1; rewrite E1 rangePtUnK. - by rewrite {1}E2 domPtUnK //; [case | rewrite -E2]. - by rewrite -E1. apply/allP=>x; rewrite domF inE D1 inE eq_sym. by case: eqP=>//= _; apply/allP/A1. have {}H x1 w1 x2 w2 t1 t2 : (x1, x2) \In phi2 -> (x1, w1) \In f1 -> (x2, w2) \In free f2 k2 -> P t1 t2 -> P (if p1 (x1, w1) then a1 t1 x1 w1 else t1) (if p2 (x2, w2) then a2 t2 x2 w2 else t2). - case/InF=>_ _ F1 F2 /InF [_ _ F3]. by apply: H F1 _ F3; apply/(InPtUnE _ W); right. by case: ifP Hp=>L1; case: ifP=>L2 Hp; apply: IH M2 D2 R2' Hp H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)