proposition: Lemma remove_equiv_eval_list_is_sound : forall p l1 l2, match remove_equiv_eval_list p l1 l2 with | Some (l1',l2') => exists ll, (forall t1 t2, In (t1,t2) ll -> p t1 t2 = Some true) /\ list_permut.permut0 (@eq term) l1 (l1' ++ (map (fun st => fst st) ll)) /\ list_permut.permut0 (@eq term) l2 (l2' ++ (map (fun st => snd st) ll)) /\ (forall t1 t2, In t1 l1' -> In t2 l2' -> p t1 t2 = Some false) | None => exists t1, exists t2, In t1 l1 /\ In t2 l2 /\ p t1 t2 = None end.
proof: Proof. intros p l1 l2; functional induction (remove_equiv_eval_list p l1 l2) as [ l1 | H1 l2 H2 H3 H4 H' | H1 l2 t1 l1 H2 H3 H4 H' l2' H IH | H1 l2 t1 l1 H2 H3 H4 H' H IH l1' l2' R | H1 l2 t1 l1 H2 H3 H4 H' H IH R | H1 l2 t1 l1 H2 H3 H4 H' H]. exists (@nil (term * term)); simpl; intuition; intros. rewrite <- app_nil_end; apply list_permut.permut_refl; intro; trivial. destruct l2 as [ | t2 l2]. contradiction. exists (@nil (term * term)); simpl; intuition; intros. rewrite <- app_nil_end; apply list_permut.permut_refl; intro; trivial. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K. destruct K as [t2' [pt1t2_eq_true P]]. destruct (remove_equiv_eval_list p l1 l2') as [ [l1'' l2''] | ]. destruct IH as [ll [E_ll [P1 [P2 F]]]]; exists ((t1,t2') :: ll); repeat split; trivial. intros u1 u2 [u1u2_eq_t1t2' | u1u2_in_ll]. injection u1u2_eq_t1t2'; intros; subst; apply pt1t2_eq_true. apply E_ll; trivial. simpl; apply Pcons; trivial. apply list_permut.permut_trans with (t2' :: l2'). intros a b c _ a_eq_b b_eq_c; transitivity b; trivial. trivial. simpl. apply Pcons. trivial. trivial. destruct IH as [t1' [t2 [t1_in_l1 [t2_in_l2 p1p2_eq_none]]]]; exists t1'; exists t2; repeat split; trivial. right; trivial. destruct (list_permut.permut_inv_right P) as [t2'' [k2 [k2' [t2''_eq_t2' [H'' P']]]]]. subst l2; apply in_insert. generalize (k2 ++ k2') l2' t2_in_l2 P'; intro k; induction k as [ | u k]; intros l t2_in_l Q; inversion Q as [ | a b k' l1' l2]; subst; trivial. destruct (in_app_or _ _ _ t2_in_l) as [t2_in_l1' | [t2_eq_b | t2_in_l2']]. right; apply (IHk (l1' ++ l2)); trivial; apply in_or_app; left; trivial. left; subst; trivial. right; apply (IHk (l1' ++ l2)); trivial; apply in_or_app; right; trivial. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K. rewrite R in IH; destruct IH as [ll [E_ll [P1 [P2 F]]]]; exists ll; repeat split; auto. simpl. apply (Pcons (R := @eq term) t1 t1 (l := l1) nil (l1' ++ map (fun st : term * term => fst st) ll)); trivial. simpl; intros u1 u2 [u1_eq_t1 | u1_in_l1'] u2_in_l2'. subst u1; apply K; rewrite (in_permut_in P2); apply in_or_app; left; trivial. apply F; trivial. rewrite R in IH; destruct IH as [u1 [u2 [u1_in_l1 [u2_in_l2 pu1u2_eq_none]]]]; exists u1; exists u2; repeat split; trivial; right; trivial. assert (K := remove_equiv_eval_is_sound p t1 l2); rewrite H in K. destruct K as [t2 [t2_in_l2 pt1t2_eq_none]]; exists t1; exists t2; repeat split; trivial; left; trivial. Qed.
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)