Skip to content

Instantly share code, notes, and snippets.

@JasonGross

JasonGross/ltac_big_mem.v

Last active December 22, 2017 18:31
Show Gist options
  • Save JasonGross/e3d55b61a26e038020870df825cd0896 to your computer and use it in GitHub Desktop.
Save JasonGross/e3d55b61a26e038020870df825cd0896 to your computer and use it in GitHub Desktop.
Download ZIP
ltac_slow_fresh.v
Raw
ltac_big_mem.v
Global Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
(at level 200, x binder, y binder, f at level 200, format "'dlet' x .. y := v 'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
(at level 200, f at level 200, format "'elet' x := v 'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
:= let x := v in f x.
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
Inductive expr {var : Type} : Type :=
| NatO : expr
| NatS : expr -> expr
| LetIn (v : expr) (f : var -> expr)
| Var (v : var)
| NatMul (x y : expr).
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with expr.
Infix "*" := NatMul : expr_scope.
Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
Notation "$$ x" := (Var x) (at level 9, format "$$ x") : expr_scope.
Fixpoint denote (e : @expr nat) : nat
:= match e with
| NatO => O
| NatS x => S (denote x)
| LetIn v f => dlet x := denote v in denote (f x)
| Var v => v
| NatMul x y => denote x * denote y
end.
Definition Expr := forall var, @expr var.
Definition Denote (e : Expr) := denote (e _).
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
Add Printing Let prod.
Arguments pair {A B} _ _.
Arguments fst {A B} _.
Arguments snd {A B} _.
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
(* cf COQBUG(https://github.com/coq/coq/issues/5448), COQBUG(https://github.com/coq/coq/issues/6315) *)
Ltac refresh n :=
let n' := fresh n in
let n' := fresh n in
n'.
Ltac Reify_of reify x :=
constr:(fun var : Type => ltac:(let v := reify var x in exact v)).
Ltac error_cant_elim_deps f :=
let __ := match goal with
| _ => idtac "Failed to eliminate functional dependencies in" f
end in
constr:(I : I).
Ltac error_bad_function f :=
let __ := match goal with
| _ => idtac "Bad let-in function" f
end in
constr:(I : I).
Ltac error_bad_term term :=
let __ := match goal with
| _ => idtac "Unrecognized term:" term
end in
let ret := constr:(term : I) in
constr:(I : I).
Ltac reify var term :=
let reify_rec term := reify var term in
lazymatch term with
| fst (?term, ?v)
=> constr:(@Var var v)
| _
=>
lazymatch term with
| O => constr:(@NatO var)
| S ?x
=> let rx := reify_rec x in
constr:(@NatS var rx)
| ?x * ?y
=> let rx := reify_rec x in
let ry := reify_rec y in
constr:(@NatMul var rx ry)
| (dlet x := ?v in ?f)
=> let rv := reify_rec v in
let not_x := refresh x in
let not_x2 := refresh not_x in
let not_x3 := refresh not_x2 in
let rf
:=
lazymatch
constr:(
fun (not_x : nat) (not_x2 : var)
=> match @fst nat var (@pair nat var not_x not_x2) return @expr var with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return] *)
| x
=> match f return @expr var with
| not_x3
=> ltac:(let fx := (eval cbv delta [not_x3 x] in not_x3) in
clear x not_x3;
let rf := reify_rec fx in
exact rf)
end
end)
with
| fun _ => ?f => f
| ?f => error_cant_elim_deps f
end in
constr:(@LetIn var rv rf)
| ?v
=> error_bad_term v
end
end.
Ltac Reify x := Reify_of reify x.
Fixpoint big (a : nat) (sz : nat) : nat
:= match sz with
| O => a
| S sz' => dlet a' := a * a in big a' sz'
end.
Notation sz := 300 (only parsing).
Goal True.
Time do 200
time (idtac;
let v := constr:(ltac:(assert (exists e, e = big 1 sz);
[ eexists;
lazy [big];
let x := match goal with |- _ = ?RHS => RHS end in
let rv := Reify x in
transitivity (Denote rv);
[ | lazy [Denote denote]; reflexivity ];
reflexivity
| exact I ])) in
idtac).
Raw
ltac_slow_fresh.v
Global Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
(at level 200, x binder, y binder, f at level 200, format "'dlet' x .. y := v 'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
(at level 200, f at level 200, format "'elet' x := v 'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
:= let x := v in f x.
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).
Inductive expr {var : Type} : Type :=
| NatO : expr
| NatS : expr -> expr
| LetIn (v : expr) (f : var -> expr)
| Var (v : var)
| NatMul (x y : expr).
Bind Scope expr_scope with expr.
Delimit Scope expr_scope with expr.
Infix "*" := NatMul : expr_scope.
Notation "'elet' x := v 'in' f" := (LetIn v (fun x => f%expr)) : expr_scope.
Notation "$$ x" := (Var x) (at level 9, format "$$ x") : expr_scope.
Fixpoint denote (e : @expr nat) : nat
:= match e with
| NatO => O
| NatS x => S (denote x)
| LetIn v f => dlet x := denote v in denote (f x)
| Var v => v
| NatMul x y => denote x * denote y
end.
Definition Expr := forall var, @expr var.
Definition Denote (e : Expr) := denote (e _).
Set Primitive Projections.
Record prod A B := pair { fst : A ; snd : B }.
Add Printing Let prod.
Arguments pair {A B} _ _.
Arguments fst {A B} _.
Arguments snd {A B} _.
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
(* cf COQBUG(https://github.com/coq/coq/issues/5448), COQBUG(https://github.com/coq/coq/issues/6315) *)
Ltac refresh n :=
let n' := fresh n in
let n' := fresh n in
n'.
Ltac Reify_of reify x :=
constr:(fun var : Type => ltac:(let v := reify var x in exact v)).
Ltac error_cant_elim_deps f :=
let __ := match goal with
| _ => idtac "Failed to eliminate functional dependencies in" f
end in
constr:(I : I).
Ltac error_bad_function f :=
let __ := match goal with
| _ => idtac "Bad let-in function" f
end in
constr:(I : I).
Ltac error_bad_term term :=
let __ := match goal with
| _ => idtac "Unrecognized term:" term
end in
let ret := constr:(term : I) in
constr:(I : I).
Ltac reify var term :=
let reify_rec term := reify var term in
lazymatch term with
| fst (?term, ?v)
=> constr:(@Var var v)
| _
=>
lazymatch term with
| O => constr:(@NatO var)
| S ?x
=> let rx := reify_rec x in
constr:(@NatS var rx)
| ?x * ?y
=> let rx := reify_rec x in
let ry := reify_rec y in
constr:(@NatMul var rx ry)
| (dlet x := ?v in ?f)
=> let rv := reify_rec v in
let not_x := refresh x in
let not_x2 := refresh not_x in
let not_x3 := refresh not_x2 in
let rf
:=
lazymatch
constr:(
fun (not_x : nat) (not_x2 : var)
=> match fst (not_x, not_x2) return _ with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return _] *)
| x
=> match f return _ with
| not_x3
=> ltac:(let fx := (eval cbv delta [not_x3 x] in not_x3) in
let rf := reify_rec fx in
exact rf)
end
end)
with
| fun _ => ?f => f
| ?f => error_cant_elim_deps f
end in
constr:(@LetIn var rv rf)
| ?v
=> error_bad_term v
end
end.
Ltac Reify x := Reify_of reify x.
Module var_context.
Inductive var_context {var : Type} := nil | cons (n : nat) (v : var) (xs : var_context).
End var_context.
Ltac reify_helper var term ctx :=
let reify_rec term := reify_helper var term ctx in
lazymatch ctx with
| context[var_context.cons term ?v _]
=> constr:(@Var var v)
| _
=>
lazymatch term with
| O => constr:(@NatO var)
| S ?x
=> let rx := reify_rec x in
constr:(@NatS var rx)
| ?x * ?y
=> let rx := reify_rec x in
let ry := reify_rec y in
constr:(@NatMul var rx ry)
| (dlet x := ?v in ?f)
=> let rv := reify_rec v in
let not_x := refresh x in
let not_x2 := refresh not_x in
let not_x3 := refresh not_x2 in
let rf
:=
lazymatch
constr:(
fun (x : nat) (not_x : var)
=> match f, @var_context.cons var x not_x ctx return _ with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return _] *)
| not_x2, not_x3
=> ltac:(let fx := (eval cbv delta [not_x2] in not_x2) in
let ctx := (eval cbv delta [not_x3] in not_x3) in
let rf := reify_helper var fx ctx in
exact rf)
end)
with
| fun _ => ?f => f
| ?f => error_cant_elim_deps f
end in
constr:(@LetIn var rv rf)
| ?v
=> error_bad_term v
end
end.
Ltac reify2 var x :=
reify_helper var x (@var_context.nil var).
Ltac Reify2 x := Reify_of reify2 x.
Ltac reify_helper' var term ctx :=
let reify_rec term := reify_helper' var term ctx in
lazymatch ctx with
| context[var_context.cons term ?v _]
=> constr:(@Var var v)
| _
=>
lazymatch term with
| O => constr:(@NatO var)
| S ?x
=> let rx := reify_rec x in
constr:(@NatS var rx)
| ?x * ?y
=> let rx := reify_rec x in
let ry := reify_rec y in
constr:(@NatMul var rx ry)
| (dlet x := ?v in ?f)
=> let rv := reify_rec v in
let not_x := refresh x in
let not_x2 := refresh not_x in
let not_x3 := refresh not_x2 in
let rf
:=
lazymatch
constr:(
fun (x : nat) (not_x : var)
=> match f return _ with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return _] *)
| not_x2
=> ltac:(let fx := (eval cbv delta [not_x2] in not_x2) in
let ctx := constr:(@var_context.cons var x not_x ctx) in
let rf := reify_helper' var fx ctx in
exact rf)
end)
with
| fun _ => ?f => f
| ?f => error_cant_elim_deps f
end in
constr:(@LetIn var rv rf)
| ?v
=> error_bad_term v
end
end.
Ltac reify2' var x :=
reify_helper' var x (@var_context.nil var).
Ltac Reify2' x := Reify_of reify2' x.
Definition var_for {var : Type} (n : nat) (v : var) := False.
Ltac reify3 var term :=
let reify_rec term := reify3 var term in
lazymatch goal with
| [ H : var_for term ?v |- _ ]
=> constr:(@Var var v)
| _
=>
lazymatch term with
| O => constr:(@NatO var)
| S ?x
=> let rx := reify_rec x in
constr:(@NatS var rx)
| ?x * ?y
=> let rx := reify_rec x in
let ry := reify_rec y in
constr:(@NatMul var rx ry)
| (dlet x := ?v in ?f)
=> let rv := reify_rec v in
let not_x := refresh x in
let not_x2 := refresh not_x in
let rf
:=
lazymatch
constr:(
fun (x : nat) (not_x : var) (_ : @var_for var x not_x)
=> match f return _ with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return _] *)
| not_x2
=> ltac:(let fx := (eval cbv delta [not_x2] in not_x2) in
let rf := reify_rec fx in
exact rf)
end)
with
| fun _ v' _ => @?f v' => f
| ?f => error_cant_elim_deps f
end in
constr:(@LetIn var rv rf)
| ?v
=> error_bad_term v
end
end.
Ltac Reify3 x := Reify_of reify3 x.
Fixpoint big (a : nat) (sz : nat) : nat
:= match sz with
| O => a
| S sz' => dlet a' := a * a in big a' sz'
end.
Notation sz := 200 (only parsing).
Goal exists e, e = big 1 sz.
Time eexists; cbv [big].
Time let x := match goal with |- _ = ?RHS => RHS end in
let rv := Reify x in
(*transitivity (Denote rv)*)
idtac. (* 3.03 s *)
Time let x := match goal with |- _ = ?RHS => RHS end in
let rv := Reify2 x in
(*transitivity (Denote rv)*)
idtac. (* 2.3 s *)
Time let x := match goal with |- _ = ?RHS => RHS end in
let rv := Reify2' x in
(*transitivity (Denote rv)*)
idtac. (* 1.5 s *)
Time let x := match goal with |- _ = ?RHS => RHS end in
let rv := Reify3 x in
(*transitivity (Denote rv)*)
idtac. (* 1.4 s *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment