Stream: Coq users

Topic: Rewrite not working


view this post on Zulip Lessness (Dec 05 2021 at 17:39):

A rewrite squared_length_S in H at the end not working. I can use replace with reflexivity and it works, but rewrite doesn't.
Any ideas what's going on?

Require Import Reals Lra Field List Lia Classical Utf8.
Set Implicit Arguments.
Open Scope R.

Fixpoint type_pow (n: nat) (x: Set): Set :=
  match n with
  | O => unit
  | 1 => x
  | S m => prod (type_pow m x) x
  end.
Notation "x ^ n" := (type_pow n x).

Definition vector_mult {n} (k: R) (x: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (k * x).
  + destruct x as [tx x]. exact (IHn tx, k * x).
Defined.

Definition vector_sum {n} (x y: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (x + y).
  + destruct x as [tx x], y as [ty y]. exact (IHn tx ty, x + y).
Defined.

Definition vector_difference {n} (x y: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (x - y).
  + destruct x as [tx x], y as [ty y]. exact (IHn tx ty, x - y).
Defined.

Definition elementwise_product {n} (x y: R^(S n)): R^(S n).
Proof.
  induction n.
  + exact (x * y).
  + destruct x as [tx x], y as [ty y]. exact (IHn tx ty, x * y).
Defined.

Definition vector_element_sum {n} (x: R^(S n)): R.
Proof.
  induction n.
  + exact x.
  + destruct x as [tx x]. exact (IHn tx + x).
Defined.

Definition scalar_mult {n} (x y: R^(S n)): R := vector_element_sum (elementwise_product x y).
Definition scalar_mult_S {n} (tx ty: R^(S n)) (x y: R): @scalar_mult (S n) (tx, x) (ty, y) = scalar_mult tx ty + x * y.
Proof.
  reflexivity.
Qed.

Definition squared_length {n} (x: R^(S n)): R := scalar_mult x x.
Definition squared_length_S {n} (tx: R^(S n)) (x: R): @squared_length (S n) (tx, x) = squared_length tx + x * x.
Proof.
  reflexivity.
Qed.

Definition squared_length_nonneg {n} (x: R^(S n)): 0 <= squared_length x.
Proof.
  induction n.
  + apply Rle_0_sqr.
  + destruct x as [tx x]. rewrite squared_length_S. pose proof (IHn tx). pose proof (Rle_0_sqr x). unfold Rsqr in H0. lra.
Qed.

Definition length {n} (x: R^(S n)): R :=
  Rsqrt (mknonnegreal _ (squared_length_nonneg x)).

Theorem squared_length_thm {n} (x: R^(S n)): squared_length x = length x * length x.
Proof.
  unfold length. rewrite Rsqrt_Rsqrt. simpl. auto.
Qed.

Theorem length_nonneg {n} (x: R^(S n)): 0 <= length x.
Proof.
  apply Rsqrt_positivity.
Qed.

Definition distance {n} (x y: R^(S n)): R := length (vector_difference x y).

Theorem distance_nonneg {n} (x y: R^(S n)): 0 <= distance x y.
Proof.
  apply Rsqrt_positivity.
Qed.

Theorem Rsqrt_of_square (x: R) (H: 0 <= x * x): Rsqrt (mknonnegreal (x * x) H) = Rabs x.
Proof.
  apply Rsqr_inj.
  + apply Rsqrt_positivity.
  + unfold Rabs. destruct Rcase_abs; lra.
  + unfold Rsqr. rewrite Rsqrt_Rsqrt. simpl. apply Rsqr_abs.
Qed.

Theorem Rsqrt_eq_zero_iff (x: R) (H: 0 <= x): Rsqrt (mknonnegreal x H) = 0  x = 0.
Proof.
  split; intros.
  + pose (Rsqrt_Rsqrt (mknonnegreal x H)). rewrite H0 in e. simpl in e. lra.
  + assert (x = 0 * 0) by (unfold Rsqr; lra). clear H0. subst. rewrite Rsqrt_of_square.
    unfold Rabs. destruct Rcase_abs; lra.
Qed.

Theorem distance_zero_iff {n: nat} (x y: R^(S n)): distance x y = 0  x = y.
Proof.
  split; intros.
  + induction n.
    - apply Rsqrt_eq_zero_iff in H. apply Rsqr_0_uniq in H. simpl in H. lra.
    - destruct x as [tx x], y as [ty y]. apply Rsqrt_eq_zero_iff in H.
      simpl in H. try rewrite squared_length_S in H.
Admitted.

view this post on Zulip Li-yao (Dec 05 2021 at 18:09):

Interestingly rewrite @squared_length_S goes through.

view this post on Zulip Lessness (Dec 07 2021 at 02:07):

Li-yao said:

Interestingly rewrite @squared_length_S goes through.

Ok, that's good enough for me. Thank you!


Last updated: Jan 28 2023 at 06:30 UTC