Mukesh Tiwari (Apr 08 2022 at 09:55): 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)
*)
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.
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.
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: Apr 20 2024 at 02:40 UTC