Stream: Coq users

Topic: Proving two functions (polynomials) are same.


view this post on Zulip 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.

  Add Field cField : Rfield.
  Add Ring cRing : RRing.

  (* 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.
    admit.
  + simpl.
    intros ?.
    assert (length l - length l = 0)%nat.
    nia.
    rewrite H.
    simpl.
    ring_simplify.
    rewrite <-IHl.
    unfold add_rlist,
    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)]

    Now, if I add both
    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)


  *)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Apr 08 2022 at 10:45):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mukesh Tiwari (Apr 08 2022 at 11:35):

Thank you very much. It's very helpful.

view this post on Zulip 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: Jan 31 2023 at 13:02 UTC