Require Import List Reals.
Open Scope R_scope.
Definition fib_aux :=
nat_rect (fun _ => list R) (0 :: 1 :: nil)
(fun _ v => (nth 1 v 0 :: nth 0 v 0 + nth 1 v 0 :: nil))
.
Definition fib (n : nat) : R :=
nth 0 (fib_aux n) 0.
Lemma big_fib1 : fib 10 = 55.
Proof.
unfold fib; simpl; ring.
Qed.
Lemma big_fib : fib 11 = 89.
Proof.
unfold fib; simpl.
ring_simplify.
With Vscoq>Proof:Mode set to settings.
When I do alt-rightarrow to line 14, then alt-downarrow, then 4 times alt-uparrow, I get the "executed zone" colored down to line 15 (should be to line 11 or 12).
With the following file as playground.
With Vscoq>Proof:Mode set to settings. When I do alt-rightarrow to line 14, then alt-downarrow, then 4 times alt-uparrow, I get the "executed zone" colored down to line 15 (should be to line 11 or 12).
Here is an animation showing this unwanted behavior https://filesender.renater.fr/?s=download&token=d76d35d8-2abf-48cd-9593-4c0ca0b4574a