proposition: Lemma to_rformP e f : holds e (to_rform f) <-> holds e f.
proof: Proof. suffices{e f} equal0_equiv e t1 t2: holds e (eq0_rform (t1 - t2)) <-> (eval e t1 == eval e t2). - elim: f e => /=; try tauto. + move=> t1 t2 e. by split; [move/equal0_equiv/eqP | move/eqP/equal0_equiv]. + by move=> t1 e; rewrite unitrE; apply: equal0_equiv. + by move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. + by move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. + by move=> f1 IHf1 f2 IHf2 e; move: (IHf1 e) (IHf2 e); tauto. + by move=> f1 IHf1 e; move: (IHf1 e); tauto. + by move=> n f1 IHf1 e; split=> [] [x] /IHf1; exists x. + by move=> n f1 IHf1 e; split=> Hx x; apply/IHf1. rewrite -(add0r (eval e t2)) -(can2_eq (subrK _) (addrK _)). rewrite -/(eval e (t1 - t2)); move: (t1 - t2)%T => {t1 t2} t. have sub_var_tsubst s t0: s.1 >= ub_var t0 -> tsubst t0 s = t0. elim: t0 {t} => //=. - by move=> n; case: ltngtP. - by move=> t1 IHt1 t2 IHt2; rewrite geq_max => /andP[/IHt1-> /IHt2->]. - by move=> t1 IHt1 /IHt1->. - by move=> t1 IHt1 n /IHt1->. - by move=> t1 IHt1 t2 IHt2; rewrite geq_max => /andP[/IHt1-> /IHt2->]. - by move=> t1 IHt1 /IHt1->. - by move=> t1 IHt1 n /IHt1->. pose fix rsub t' m r : term R := if r is u :: r' then tsubst (rsub t' m.+1 r') (m, u^-1)%T else t'. pose fix ub_sub m r : Prop := if r is u :: r' then ub_var u <= m /\ ub_sub m.+1 r' else true. suffices{t} rsub_to_r t r0 m: m >= ub_var t -> ub_sub m r0 -> let: (t', r) := to_rterm t r0 m in [/\ take (size r0) r = r0, ub_var t' <= m + size r, ub_sub m r & rsub t' m r = t]. - have:= rsub_to_r t [::] _ (leqnn _); rewrite /eq0_rform. case: (to_rterm _ _ _) => [t1' r1] [//|_ _ ub_r1 def_t]. rewrite -{2}def_t {def_t}. elim: r1 (ub_var t) e ub_r1 => [|u r1 IHr1] m e /= => [_|[ub_u ub_r1]]. by split=> /eqP. rewrite eval_tsubst /=; set y := eval e u; split=> t_eq0. apply/IHr1=> //; apply: t_eq0. rewrite nth_set_nth /= eqxx -(eval_tsubst e u (m, Const _)). rewrite sub_var_tsubst //= -/y. case Uy: (y \in unit); [left | right]; first by rewrite mulVr ?divrr. split=> [|[z]]; first by rewrite invr_out ?Uy. rewrite nth_set_nth /= eqxx. rewrite -!(eval_tsubst _ _ (m, Const _)) !sub_var_tsubst // -/y => yz1. by case/unitrP: Uy; exists z. move=> x def_x; apply/IHr1=> //; suff ->: x = y^-1 by []; move: def_x. rewrite nth_set_nth /= eqxx -(eval_tsubst e u (m, Const _)). rewrite sub_var_tsubst //= -/y; case=> [[xy1 yx1] | [xy nUy]]. by rewrite -[y^-1]mul1r -[1]xy1 mulrK //; apply/unitrP; exists x. rewrite invr_out //; apply/unitrP=> [[z yz1]]; case: nUy; exists z. rewrite nth_set_nth /= eqxx -!(eval_tsubst _ _ (m, _%:T)%T). by rewrite !sub_var_tsubst. have rsub_id r t0 n: ub_var t0 <= n -> rsub t0 n r = t0. by elim: r n => //= t1 r IHr n let0n; rewrite IHr ?sub_var_tsubst ?leqW. have rsub_acc r s t1 m1: ub_var t1 <= m1 + size r -> rsub t1 m1 (r ++ s) = rsub t1 m1 r. elim: r t1 m1 => [|t1 r IHr] t2 m1 /=; first by rewrite addn0; apply: rsub_id. by move=> letmr; rewrite IHr ?addSnnS. elim: t r0 m => /=; try do [ by move=> n r m hlt hub; rewrite take_size (ltn_addr _ hlt) rsub_id | by move=> n r m hlt hub; rewrite leq0n take_size rsub_id | move=> t1 IHt1 t2 IHt2 r m; rewrite geq_max; case/andP=> hub1 hub2 hmr; case: to_rterm {hub1 hmr}(IHt1 r m hub1 hmr) => t1' r1; case=> htake1 hub1' hsub1 <-; case: to_rterm {IHt2 hub2 hsub1}(IHt2 r1 m hub2 hsub1) => t2' r2 /=; rewrite geq_max; case=> htake2 -> hsub2 /= <-; rewrite -{1 2}(cat_take_drop (size r1) r2) htake2; set r3 := drop _ _; rewrite size_cat addnA (leq_trans _ (leq_addr _ _)) //; split=> {hsub2}//; first by [rewrite takel_cat // -htake1 size_take geq_min leqnn orbT]; rewrite -(rsub_acc r1 r3 t1') {hub1'}// -{htake1}htake2 {r3}cat_take_drop; by elim: r2 m => //= u r2 IHr2 m; rewrite IHr2 | do [ move=> t1 IHt1 r m; do 2!move=> /IHt1{}IHt1 | move=> t1 IHt1 n r m; do 2!move=> /IHt1{}IHt1]; case: to_rterm IHt1 => t1' r1 [-> -> hsub1 <-]; split=> {hsub1}//; by elim: r1 m => //= u r1 IHr1 m; rewrite IHr1]. move=> t1 IH r m letm /IH {IH} /(_ letm) {letm}. case: to_rterm => t1' r1 /= [def_r ub_t1' ub_r1 <-]. rewrite size_rcons addnS leqnn -{1}cats1 takel_cat ?def_r; last first. by rewrite -def_r size_take geq_min leqnn orbT. elim: r1 m ub_r1 ub_t1' {def_r} => /= [|u r1 IHr1] m => [_|[->]]. by rewrite addn0 eqxx. by rewrite -addSnnS => /IHr1 IH /IH[_ _ ub_r1 ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)