## Stream: Coq users

### Topic: Rewrite not working

#### 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.
``````

#### Li-yao (Dec 05 2021 at 18:09):

Interestingly `rewrite @squared_length_S` goes through.

#### 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