## Stream: Coq users

### Topic: Proving two functions (polynomials) are same.

#### Mukesh Tiwari (Apr 08 2022 at 09:55):

Hi everyone,

I am trying to prove that two functions, `mul_closed_poly` and `compute_poly_simp`, evaluates to the same value (see the lemma `comp_gen`). However, whenever I am trying to prove it for an arbitrary list, by induction on list l, it's pretty messy (and scary :)). I am wondering if there is something like this in Coq library or someone has already proved it. Any comment will be very helpful.

Best,
Mukesh

``````Require Import Field_theory
Ring_theory List NArith
Ring Field Utf8 Lia.
Import ListNotations.

Section Computation.

Variable
(R : Type)
(rO rI:R)
(radd rmul rsub : R -> R -> R)
(ropp : R -> R)
(rdiv : R -> R -> R)
(rinv : R -> R).

Variable RRing :
ring_theory rO rI radd rmul rsub ropp eq.
Variable Rfield :
field_theory rO rI radd rmul rsub ropp rdiv rinv eq.

(* power theory *)
Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul eq Cp_phi rpow.

(* Field notations *)
Local Notation "0" := rO : R_scope.
Local Notation "1" := rI : R_scope.
Local Infix "+" := radd : R_scope.
Local Infix "-" := rsub : R_scope.
Local Infix "*" := rmul : R_scope.
Local Infix "/" := rdiv : R_scope.
Notation "- x" := (ropp x) : R_scope.
Notation "/ x" := (rinv x) : R_scope.

Local Open Scope R_scope.

(* closed form of polynomial *)
Fixpoint mul_closed_poly (l : list R) (x : R) : R :=
match l with
| [] => 1
| h :: t => (h - x) * mul_closed_poly t x
end.

(* generate k combinations of list l *)
Fixpoint gen_comb (l : list R) (k : nat) : list (list R) :=
match k with
| O => [[]]
| S k' => match l with
| [] => []
| h :: t => List.map (fun u => h :: u) (gen_comb t k') ++
gen_comb t k
end
end.

Definition add_rlist (l : list R) :=
List.fold_left (λ a b, a + b) l 0.

Definition mul_rlist (l : list R) :=
List.fold_left (λ a b, a * b) l 1.

(* expanded form of polynomial *)
Fixpoint compute_poly_simp (l : list R)
(x : R) (k : nat) : R :=
match k with
| O => pow_N 1 rmul (-x) (N.of_nat (List.length l))
| S k' => (pow_N 1 rmul (-x) (N.of_nat (Nat.sub (List.length l) k))) *
(add_rlist (List.map mul_rlist (gen_comb l k))) +
compute_poly_simp l x k'
end.

Variable x x₁ x₂ x₃ x₄ : R.

Lemma comp_gen :
compute_poly_simp [x₁; x₂] x 2 =
mul_closed_poly [x₁; x₂] x.
Proof.
compute.
ring_simplify.
ring.
Qed.

Lemma compute_simp :
forall l x,
compute_poly_simp l x (List.length l) =
mul_closed_poly l x.
Proof.
induction l.
+ simpl.
+ simpl.
intros ?.
assert (length l - length l = 0)%nat.
nia.
rewrite H.
simpl.
ring_simplify.
rewrite <-IHl.
mul_rlist.

(*
Proof idea :
Induction is going to mess the structure,
so I need to keep everything in a list.

If I have an expanded terms of
fnx := (x₁ - x) (x₂ - x) .... (xn - x)
Now, I am going to multiply fnx by
fnx * (xn+1 - x).

fnx * xn+1 - fnx * x

(x₁ - x) * (x₂ - x)
= [(0, 2, 1,  x₁ * x₂);
(1, 1, - x, x₁ + x₂);
(2, 0, - x * - x, 1)]
: list (nat * nat * R * R)

Step 1: Now, I am going to multiply by x₃
(x₁ - x) * (x₂ - x) * x₃
= [(0, 3, 1,  x₁ * x₂ * x₃);
(1, 2, - x, x₁ * x₃ + x₂ * x₃);
(2, 1, - x * - x, x₃)]

Step 2: I am going to mutiply by (-x)
(x₁ - x) * (x₂ - x) * (-x)
= [(1, 2, - x,  x₁ * x₂);
(2, 1, - x * - x, x₁ + x₂);
(3, 0, - x * - x * - x, 1)]

matrices their entries, keep x as it is:
[(0, 3, 1,  x₁ * x₂ * x₃);
(1, 2, - x, x₁ * x₃ + x₂ * x₃ + x₁ * x₂);
(2, 1, - x * - x, x₃ + x₁ + x₂);
(3, 0, - x * - x * - x, 1)]
And this expression is the same as the below one

(x₁ - x) * ((x₂ - x) * ((x₃ - x) * 1))
= [(0, 3, 1, 0 + 1 * x₁ * x₂ * x₃);
(1, 2, - x, 0 + 1 * x₁ * x₂ + 1 * x₁ * x₃ + 1 * x₂ * x₃);
(2, 1, - x * - x, 0 + 1 * x₁ + 1 * x₂ + 1 * x₃);
(3, 0, - x * (- x * - x), 0 + 1)]
: list (nat * nat * R * R)

*)
``````

#### Gaëtan Gilbert (Apr 08 2022 at 10:13):

your theorem talks about `compute_poly_simp l x (List.length l)` but the recursive call in compute_poly_simp is on `l` and some nat which is not its length
you need to find some lemma to prove about `compute_poly_simp l x n` by induction on n which when n = List.length l implies your theorem

#### Mukesh Tiwari (Apr 08 2022 at 10:17):

Yeah, you are right, I need some generalisation. I just figured out that it's true for every `n` that is greater than or equal to length of list `l`. Hopefully, this may lead to something nicer.

``````Lemma compute_simp :
forall n l x,
(List.length l <= n)%nat ->
compute_poly_simp l x n =
mul_closed_poly l x.
``````

#### Gaëtan Gilbert (Apr 08 2022 at 10:45):

no, compute_poly_simp recurses on n smaller than the length of l

#### Mukesh Tiwari (Apr 08 2022 at 11:19):

I don't get what do you mean by `compute_poly_simp recurses on n smaller than the length of l`? I was too quick to respond, but when you said `your theorem talks about compute_poly_simp l x (List.length l) but **the recursive call in compute_poly_simp is on l** and some nat which is not its length`, but the recursive call on a `k` and not on `l` so what am I missing here? Thanks for your time and patience!

You mean the lemma, or I need something like this?

``````Lemma compute_simp :
forall n l x,
(n <= List.length l)%nat ->
SOME-EXTRA-COMPUTATION-IN-TERMS-OF-l-n-x +  compute_poly_simp l x n =
mul_closed_poly l x.
``````

#### Gaëtan Gilbert (Apr 08 2022 at 11:28):

when you prove `P n (compute_poly_simp l x n)` by induction on n, in the `S n` case you are proving `P (S n) (compute_poly_simp l x (S n))` ie

``````P (S n) (
(pow_N 1 rmul (-x) (N.of_nat (Nat.sub (List.length l) (S n)))) *
(add_rlist (List.map mul_rlist (gen_comb l (S n)))) +
compute_poly_simp l x n
)
``````

you need to be able to use your induction hypothesis for that somehow
I don't know enough to tell if `P k v := EXTRA-COMPUTATION l x k + v = mul_closed_poly l x` works

#### Gaëtan Gilbert (Apr 08 2022 at 11:34):

for instance if you have

``````  Fixpoint rev (l:list A) : list A :=
match l with
| [] => []
| x :: l' => rev l' ++ [x]
end.
``````

and you want to prove `forall l, rev (rev l) = l` you will first prove a lemma `forall l x, (rev l ++ [x]) = x :: rev l`

#### Mukesh Tiwari (Apr 08 2022 at 11:35):

Thank you very much. It's very helpful.

#### Mukesh Tiwari (Apr 08 2022 at 18:13):

I think I have figured out the invariant but still long way to go.

``````Lemma compute_simp_gen :
forall n l y,
(n <= List.length l)%nat ->
compute_poly_simp (take n l) y n *
mul_closed_poly (drop n l) y = mul_closed_poly l y.
``````

Last updated: Oct 04 2023 at 22:01 UTC