proposition: Lemma equiv_eval_list_is_sound : forall p l1 l2, match equiv_eval_list p l1 l2 with | Some true => length l1 = length l2 /\ (forall t1 t2, In (t1,t2) (combine l1 l2) -> p t1 t2 = Some true) | Some false => length l1 <> length l2 \/ (exists t1, exists t2, In (t1,t2) (combine l1 l2) /\ p t1 t2 = Some false) | None => exists t1, exists t2, In (t1,t2) (combine l1 l2) /\ p t1 t2 = None end.
proof: Proof. intros p l1; induction l1 as [ | t1 l1]; intros [ | t2 l2]; simpl. split; trivial; intros; contradiction. left; discriminate. left; discriminate. assert (H : forall u2, u2 = t2 -> p t1 u2 = p t1 t2). intros; subst; trivial. destruct (p t1 t2) as [ [ | ] | ]; generalize (H _ (eq_refl _)); clear H; intro H. generalize (IHl1 l2); destruct (equiv_eval_list p l1 l2) as [ [ | ] | ]. intros [L H']; repeat split. rewrite L; trivial. intros t3 t4 [t3t4_eq_t1t2 | t3t4_in_ll]. injection t3t4_eq_t1t2; intros; subst; trivial. apply H'; trivial. intros [L | [t3 [t4 [H' H'']]]]. left; intros H''; apply L; injection H''; intros; trivial. right; exists t3; exists t4; split; trivial; right; trivial. intros [t3 [t4 [H' H'']]]; exists t3; exists t4; split; trivial; right; trivial. right; exists t1; exists t2; split; trivial; left; trivial. exists t1; exists t2; 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)