Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/rewrite_drops_hyps.v

Created October 11, 2022 01:32
Show Gist options
  • Save Blaisorblade/1334492d63020c064b4a247c8c9a1262 to your computer and use it in GitHub Desktop.
Save Blaisorblade/1334492d63020c064b4a247c8c9a1262 to your computer and use it in GitHub Desktop.
Download ZIP
Demonstrate strange rewrite behavior
Raw
rewrite_drops_hyps.v
Require Import List.
Import ListNotations.
Lemma test1 :
length ([1] ++ [2]) = 2 ->
2 = 4.
Proof.
intros HA.
evar (N : nat).
Unshelve.
admit.
Check HA.
Undo.
Undo.
(* FIX: *)
(* clear N. *)
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.
(* evar (N : nat). *)
Unshelve.
admit.
Check HA.
Undo.
Undo.
(* FIX: *)
(* clear N. *)
rewrite -> app_length 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.
@aa755
Copy link

aa755 commented Oct 11, 2022

the following lines can be removed as they seem to be from a previous experment and dont seem to be relevant anymore

 (* evar (N : nat). *)
  (* FIX: *)
  (* clear N. *)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment