Demonstrate strange rewrite behavior

rewrite_drops_hyps.v

Require Import List.
Import ListNotations.
Require Import ssreflect.
Lemma test1 :
  length ([1] ++ [2]) = 2 ->
  2 = 4.
Proof.
  intros HA.
  evar (N : nat).
  Unshelve.
  admit.
  Check HA.
  Undo.
  Undo.
  rewrite -> app_length in HA.
  Unshelve.
  admit.
  (* Now [HA] has disappeared from the context of the second goal, unless we run [clear N]. *)
  Fail Check HA.
Abort.


Lemma test2 :
  length ([1] ++ [2]) = 2 ->
  exists n : nat, n + 4 = 2.
Proof.
  intros HA.
  eexists.
  Unshelve.
  admit.
  Check HA.
  Undo.
  Undo.
  rewrite /= in HA.
  Unshelve.
  admit.
  (* Now [HA] has disappeared from the context of the second goal, and we can't [clear N] to fix that. *)
  Fail Check HA.
Abort.

Lemma test3 :
  length ([1] ++ [2]) = 2 ->
  exists n : nat, n + 4 = 2.
Proof.
  intros HA.
  eexists.
  Unshelve.
  admit.
  Check HA.
  Undo.
  Undo.
  change (length ([1] ++ [2])) with (length [1] + length [2]) in HA.
  Unshelve.
  admit.
  (* Now [HA] is still there: *)
  Check HA.
Abort.

Definition ignore(x: Prop) := True.

Lemma test4 :
  length ([1] ++ [2]) = 2 ->
  exists n : nat, n + 4 = 2.
Proof.
  intros HA.
  eexists.
  Unshelve.
  admit.
  Check HA.
  Undo.
  Undo.
  eassert (ignore _) as P. {
    rewrite /= in HA.
    let t := type of HA in instantiate (1 := t).
    exact I.
  }
  lazymatch type of P with
  | ignore ?t => change t in HA; clear P
  end.
  Unshelve.
  admit.
  (* Now [HA] is still there (but with the old type): *)
  Check HA.
Abort.