proposition: Lemma equiv_bool_equation : forall t1 t2, equiv_bool t1 t2 = match t1, t2 with | Var v1, Var v2 => X.eq_bool v1 v2 | Var _, Term _ _ => false | Term _ _, Var _ => false | Term f1 l1, Term f2 l2 => if prec_eq_bool Prec f1 f2 then match status Prec f1 with | Lex => let equiv_lex_bool := (fix equiv_lex_bool (kk1 kk2 : list term) {struct kk1} : bool := (match kk1 with | [] => match kk2 with [] => true | _ :: _=> false end | t1 :: k1 => match kk2 with [] => false | t2 :: k2=> (equiv_bool t1 t2) && (equiv_lex_bool k1 k2) end end)) in (equiv_lex_bool l1 l2) | Mul => let equiv_mult_bool := (fix equiv_mult_bool (kk1 kk2 : list term) {struct kk1} : bool := (match kk1 with | [] => match kk2 with [] => true | _ :: _=> false end | t1 :: k1 => match remove equiv_bool t1 kk2 with None => false | Some k2 => equiv_mult_bool k1 k2 end end)) in (equiv_mult_bool l1 l2) end else false end.
proof: Proof. assert (H : forall t1 t2 k, size t1 <= k -> iter (term -> term -> bool) k equiv_bool_F equiv_bool t1 t2 = equiv_bool t1 t2). intros t1 t2 k L; unfold equiv_bool at 2; generalize (equiv_bool_terminate t1 t2). intro H; case H; clear H; intros v H; apply H; apply L. intro t1; pattern t1; apply term_rec3; clear t1. intros v1 [v2 | f2 l2]; reflexivity. intros f1 l1 IH [v2 | f2 l2]. reflexivity. rewrite <- (H (Term f1 l1) (Term f2 l2) _ (le_n _)); rewrite size_unfold; simpl. case (prec_eq_bool Prec f1 f2); [idtac | reflexivity]. case (status Prec f1); clear f1. assert (H' : forall l1 f1 f2, (forall t1, In t1 l1 -> forall t2, f1 t1 t2 = f2 t1 t2) -> forall l2, (fix equiv_lex_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match kk2 with | [] => false | t2 :: k2 => f1 t1 t2 && equiv_lex_bool k1 k2 end end) l1 l2 = (fix equiv_lex_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match kk2 with | [] => false | t2 :: k2 => f2 t1 t2 && equiv_lex_bool k1 k2 end end) l1 l2). clear l1 l2 IH; intro l1; induction l1 as [ | a1 l1]; intros g1 g2 IH [ | a2 l2]. reflexivity. reflexivity. reflexivity. apply f_equal2. apply IH; left; reflexivity. apply (IHl1 g1 g2 (tail_prop _ IH) l2). refine (H' l1 _ _ _ l2); clear H'. intros t1 t1_in_l1 t2; apply H. generalize (size_direct_subterm t1 (Term f2 l1) t1_in_l1). rewrite (size_unfold (Term f2 l1)). simpl; intro L; apply (le_S_n _ _ L). assert (H' : forall l1 f1 f2, (forall t1, In t1 l1 -> forall t2, f1 t1 t2 = f2 t1 t2) -> forall l2, (fix equiv_mult_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match remove f1 t1 kk2 with | Some k2 => equiv_mult_bool k1 k2 | None => false end end) l1 l2 = (fix equiv_mult_bool (kk1 kk2 : list term) : bool := match kk1 with | [] => match kk2 with | [] => true | _ :: _ => false end | t1 :: k1 => match remove f2 t1 kk2 with | Some k2 => equiv_mult_bool k1 k2 | None => false end end) l1 l2). clear l1 l2 IH; intro l1; induction l1 as [ | a1 l1]; intros g1 g2 IH l2. reflexivity. assert (H' : forall f1 f2, (forall t2, f1 a1 t2 = f2 a1 t2) -> forall l2, remove f1 a1 l2 = remove f2 a1 l2). clear l1 l2 g1 g2 IH IHl1; intros g1 g2 IH; induction l2 as [ | a2 l2]. reflexivity. simpl; rewrite (IH a2); rewrite IHl2; reflexivity. rewrite (H' g1 g2 (IH a1 (or_introl _ (eq_refl _)))). case (remove g2 a1 l2). intro k2; apply (IHl1 g1 g2 (tail_prop _ IH)). reflexivity. refine (H' l1 _ _ _ l2). intros t1 t1_in_l1 t2; apply H. generalize (size_direct_subterm t1 (Term f2 l1) t1_in_l1). rewrite (size_unfold (Term f2 l1)). simpl; intro L; apply (le_S_n _ _ L). Defined.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)