Merge Ltac2 plugin

11 files changed, 774 insertions, 0 deletions

diff --git a/vendor/Ltac2/tests/Makefile b/vendor/Ltac2/tests/Makefile
new file mode 100644
index 0000000000..d85ae90dd6
--- /dev/null
+++ b/vendor/Ltac2/tests/Makefile
@@ -0,0 +1,16 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqc))/
+endif
+
+all: $(patsubst %.v,%.v.log,$(wildcard *.v))
+
+%.v.log: %.v
+	$(COQBIN)/coqc -I ../src -Q ../theories Ltac2 $< > $@
+	if [ $$? = 0 ]; then \
+		echo "    $<... OK"; \
+	else \
+		echo "    $<... FAIL!"; \
+	fi; \
+
+clean:
+	rm -f *.log
diff --git a/vendor/Ltac2/tests/compat.v b/vendor/Ltac2/tests/compat.v
new file mode 100644
index 0000000000..489fa638e4
--- /dev/null
+++ b/vendor/Ltac2/tests/compat.v
@@ -0,0 +1,58 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+(** Test calls to Ltac1 from Ltac2 *)
+
+Ltac2 foo () := ltac1:(discriminate).
+
+Goal true = false -> False.
+Proof.
+foo ().
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+intros H; ltac1:(match goal with [ H : ?P |- _ ] => rewrite H end); reflexivity.
+Qed.
+
+Goal true = false -> false = true.
+Proof.
+intros H; ltac1:(rewrite H); reflexivity.
+Abort.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac2 bar nay := ltac1:(discriminate nay).
+
+Fail Ltac2 pose1 (v : constr) :=
+  ltac1:(pose $v).
+
+(** Test calls to Ltac2 from Ltac1 *)
+
+Set Default Proof Mode "Classic".
+
+Ltac foo := ltac2:(foo ()).
+
+Goal true = false -> False.
+Proof.
+ltac2:(foo ()).
+Qed.
+
+Goal true = false -> False.
+Proof.
+foo.
+Qed.
+
+(** Variables do not cross the compatibility layer boundary. *)
+Fail Ltac bar x := ltac2:(foo x).
+
+Ltac mytac tac := idtac "wow".
+
+Goal True.
+Proof.
+(** Fails because quotation is evaluated eagerly *)
+Fail mytac ltac2:(fail).
+(** One has to thunk thanks to the idtac trick *)
+let t := idtac; ltac2:(fail) in mytac t.
+constructor.
+Qed.
diff --git a/vendor/Ltac2/tests/errors.v b/vendor/Ltac2/tests/errors.v
new file mode 100644
index 0000000000..c677f6af5d
--- /dev/null
+++ b/vendor/Ltac2/tests/errors.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Ltac2.
+
+Goal True.
+Proof.
+let x := Control.plus
+  (fun () => let _ := constr:(nat -> 0) in 0)
+  (fun e => match e with Not_found => 1 | _ => 2 end) in
+match Int.equal x 2 with
+| true => ()
+| false => Control.throw (Tactic_failure None)
+end.
+Abort.
diff --git a/vendor/Ltac2/tests/example1.v b/vendor/Ltac2/tests/example1.v
new file mode 100644
index 0000000000..023791050f
--- /dev/null
+++ b/vendor/Ltac2/tests/example1.v
@@ -0,0 +1,27 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Control.
+
+(** Alternative implementation of the hyp primitive *)
+Ltac2 get_hyp_by_name x :=
+  let h := hyps () in
+  let rec find x l := match l with
+  | [] => zero Not_found
+  | p :: l =>
+    match p with
+    | (id, _, t) =>
+      match Ident.equal x id with
+      | true => t
+      | false => find x l
+      end
+    end
+  end in
+  find x h.
+
+Print Ltac2 get_hyp_by_name.
+
+Goal forall n m, n + m = 0 -> n = 0.
+Proof.
+refine (fun () => '(fun n m H => _)).
+let t := get_hyp_by_name @H in Message.print (Message.of_constr t).
+Abort.
diff --git a/vendor/Ltac2/tests/example2.v b/vendor/Ltac2/tests/example2.v
new file mode 100644
index 0000000000..c953d25061
--- /dev/null
+++ b/vendor/Ltac2/tests/example2.v
@@ -0,0 +1,281 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+Set Default Goal Selector "all".
+
+Goal exists n, n = 0.
+Proof.
+split with (x := 0).
+reflexivity.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+split with 0.
+split.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+let myvar := Std.NamedHyp @x in split with ($myvar := 0).
+split.
+Qed.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+intros H.
+eelim &H.
+split.
+Qed.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+intros H.
+elim &H with 0.
+split.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
+Proof.
+intros P H.
+Fail apply &H.
+apply &H with (m := 0).
+split.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> (0 = 1) -> P 0.
+Proof.
+intros P H e.
+apply &H with (m := 1) in e.
+exact e.
+Qed.
+
+Goal forall (P : nat -> Prop), (forall n m, n = m -> P n) -> P 0.
+Proof.
+intros P H.
+eapply &H.
+split.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+Fail constructor 1.
+constructor 1 with (x := 0).
+split.
+Qed.
+
+Goal exists n, n = 0.
+Proof.
+econstructor 1.
+split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+induction &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+induction &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+destruct &n as [|n] using nat_rect; split.
+Qed.
+
+Goal forall n, 0 + n = n.
+Proof.
+intros n.
+let n := @X in
+let q := Std.NamedHyp @P in
+destruct &n as [|$n] using nat_rect with ($q := fun m => 0 + m = m); split.
+Qed.
+
+Goal forall b1 b2, andb b1 b2 = andb b2 b1.
+Proof.
+intros b1 b2.
+destruct &b1 as [|], &b2 as [|]; split.
+Qed.
+
+Goal forall n m, n = 0 -> n + m = m.
+Proof.
+intros n m Hn.
+rewrite &Hn; split.
+Qed.
+
+Goal forall n m p, n = m -> p = m -> 0 = n -> p = 0.
+Proof.
+intros n m p He He' Hn.
+rewrite &He, <- &He' in Hn.
+rewrite &Hn.
+split.
+Qed.
+
+Goal forall n m, (m = n -> n = m) -> m = n -> n = 0 -> m = 0.
+Proof.
+intros n m He He' He''.
+rewrite <- &He by assumption.
+Control.refine (fun () => &He'').
+Qed.
+
+Goal forall n (r := if true then n else 0), r = n.
+Proof.
+intros n r.
+hnf in r.
+split.
+Qed.
+
+Goal 1 = 0 -> 0 = 0.
+Proof.
+intros H.
+pattern 0 at 1.
+let occ := 2 in pattern 1 at 1, 0 at $occ in H.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+vm_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+native_compute.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2 - 0 -> True.
+Proof.
+intros H.
+vm_compute plus in H.
+reflexivity.
+Qed.
+
+Goal 1 = 0 -> True /\ True.
+Proof.
+intros H.
+split; fold (1 + 0) (1 + 0) in H.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+cbv [ Nat.add ].
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+let x := reference:(Nat.add) in
+cbn beta iota delta [ $x ].
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+simpl beta.
+reflexivity.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+lazy.
+reflexivity.
+Qed.
+
+Goal let x := 1 + 1 - 1 in x = x.
+Proof.
+intros x.
+unfold &x at 1.
+let x := reference:(Nat.sub) in unfold Nat.add, $x in x.
+reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+exists 0, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+eexists _, 0; reflexivity.
+Qed.
+
+Goal exists x y : nat, x = y.
+Proof.
+refine '(let x := 0 in _).
+eexists; exists &x; reflexivity.
+Qed.
+
+Goal True.
+Proof.
+pose (X := True).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+pose True as X.
+constructor.
+Qed.
+
+Goal True.
+Proof.
+let x := @foo in
+set ($x := True) in * |-.
+constructor.
+Qed.
+
+Goal 0 = 0.
+Proof.
+remember 0 as n eqn: foo at 1.
+rewrite foo.
+reflexivity.
+Qed.
+
+Goal True.
+Proof.
+assert (H := 0 + 0).
+constructor.
+Qed.
+
+Goal True.
+Proof.
+assert (exists n, n = 0) as [n Hn].
++ exists 0; reflexivity.
++ exact I.
+Qed.
+
+Goal True -> True.
+Proof.
+assert (H : 0 + 0 = 0) by reflexivity.
+intros x; exact x.
+Qed.
+
+Goal 1 + 1 = 2.
+Proof.
+change (?a + 1 = 2) with (2 = $a + 1).
+reflexivity.
+Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl).
+destruct H.
+Qed.
+
+Goal (forall n, n = 0 -> False) -> False.
+Proof.
+intros H.
+specialize (H 0 eq_refl) as [].
+Qed.
diff --git a/vendor/Ltac2/tests/matching.v b/vendor/Ltac2/tests/matching.v
new file mode 100644
index 0000000000..4338cbd32f
--- /dev/null
+++ b/vendor/Ltac2/tests/matching.v
@@ -0,0 +1,71 @@
+Require Import Ltac2.Ltac2 Ltac2.Notations.
+
+Ltac2 Type exn ::= [ Nope ].
+
+Ltac2 check_id id id' := match Ident.equal id id' with
+| true => ()
+| false => Control.throw Nope
+end.
+
+Goal True -> False.
+Proof.
+Fail
+let b := { contents := true } in
+let f c :=
+  match b.(contents) with
+  | true => Message.print (Message.of_constr c); b.(contents) := false; fail
+  | false => ()
+  end
+in
+(** This fails because the matching is not allowed to backtrack once
+    it commits to a branch*)
+lazy_match! '(nat -> bool) with context [?a] => f a end.
+lazy_match! Control.goal () with ?a -> ?b => Message.print (Message.of_constr b) end.
+
+(** This one works by taking the second match context, i.e. ?a := nat *)
+let b := { contents := true } in
+let f c :=
+  match b.(contents) with
+  | true => b.(contents) := false; fail
+  | false => Message.print (Message.of_constr c)
+  end
+in
+match! '(nat -> bool) with context [?a] => f a end.
+Abort.
+
+Goal forall (i j : unit) (x y : nat) (b : bool), True.
+Proof.
+Fail match! goal with
+| [ h : ?t, h' : ?t |- _ ] => ()
+end.
+intros i j x y b.
+match! goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @x;
+  check_id h' @y
+end.
+match! reverse goal with
+| [ h : ?t, h' : ?t |- _ ] =>
+  check_id h @j;
+  check_id h' @i
+end.
+Abort.
+
+(* Check #79 *)
+Goal 2 = 3.
+  Control.plus
+    (fun ()
+     => lazy_match! goal with
+    | [ |- 2 = 3 ] => Control.zero (Tactic_failure None)
+    | [ |- 2 = _ ] => Control.zero (Tactic_failure (Some (Message.of_string "should not be printed")))
+     end)
+    (fun e
+     => match e with
+        | Tactic_failure c
+          => match c with
+             | None => ()
+             | _ => Control.zero e
+             end
+        | e => Control.zero e
+        end).
+Abort.
diff --git a/vendor/Ltac2/tests/quot.v b/vendor/Ltac2/tests/quot.v
new file mode 100644
index 0000000000..624c4ad0c1
--- /dev/null
+++ b/vendor/Ltac2/tests/quot.v
@@ -0,0 +1,26 @@
+Require Import Ltac2.Ltac2.
+
+(** Test for quotations *)
+
+Ltac2 ref0 () := reference:(&x).
+Ltac2 ref1 () := reference:(nat).
+Ltac2 ref2 () := reference:(Datatypes.nat).
+Fail Ltac2 ref () := reference:(i_certainly_dont_exist).
+Fail Ltac2 ref () := reference:(And.Me.neither).
+
+Goal True.
+Proof.
+let x := constr:(I) in
+let y := constr:((fun z => z) $x) in
+Control.refine (fun _ => y).
+Qed.
+
+Goal True.
+Proof.
+(** Here, Ltac2 should not put its variables in the same environment as
+    Ltac1 otherwise the second binding fails as x is bound but not an
+    ident. *)
+let x := constr:(I) in
+let y := constr:((fun x => x) $x) in
+Control.refine (fun _ => y).
+Qed.
diff --git a/vendor/Ltac2/tests/rebind.v b/vendor/Ltac2/tests/rebind.v
new file mode 100644
index 0000000000..e1c20a2059
--- /dev/null
+++ b/vendor/Ltac2/tests/rebind.v
@@ -0,0 +1,34 @@
+Require Import Ltac2.Ltac2 Ltac2.Notations.
+
+Ltac2 mutable foo () := constructor.
+
+Goal True.
+Proof.
+foo ().
+Qed.
+
+Ltac2 Set foo := fun _ => fail.
+
+Goal True.
+Proof.
+Fail foo ().
+constructor.
+Qed.
+
+(** Not the right type *)
+Fail Ltac2 Set foo := 0.
+
+Ltac2 bar () := ().
+
+(** Cannot redefine non-mutable tactics *)
+Fail Ltac2 Set bar := fun _ => ().
+
+(** Subtype check *)
+
+Ltac2 mutable rec f x := f x.
+
+Fail Ltac2 Set f := fun x => x.
+
+Ltac2 mutable g x := x.
+
+Ltac2 Set g := f.
diff --git a/vendor/Ltac2/tests/stuff/ltac2.v b/vendor/Ltac2/tests/stuff/ltac2.v
new file mode 100644
index 0000000000..370bc70d15
--- /dev/null
+++ b/vendor/Ltac2/tests/stuff/ltac2.v
@@ -0,0 +1,143 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 foo (_ : int) :=
+  let f (x : int) := x in
+  let _ := f 0 in
+  f 1.
+
+Print Ltac2 foo.
+
+Import Control.
+
+Ltac2 exact x := refine (fun () => x).
+
+Print Ltac2 refine.
+Print Ltac2 exact.
+
+Ltac2 foo' () := ident:(bla).
+
+Print Ltac2 foo'.
+
+Ltac2 bar x h := match x with
+| None => constr:(fun H => ltac2:(exact (hyp ident:(H))) -> nat)
+| Some x => x
+end.
+
+Print Ltac2 bar.
+
+Ltac2 qux := Some 0.
+
+Print Ltac2 qux.
+
+Ltac2 Type foo := [ Foo (int) ].
+
+Fail Ltac2 qux0 := Foo None.
+
+Ltac2 Type 'a ref := { mutable contents : 'a }.
+
+Fail Ltac2 qux0 := { contents := None }.
+Ltac2 foo0 () := { contents := None }.
+
+Print Ltac2 foo0.
+
+Ltac2 qux0 x := x.(contents).
+Ltac2 qux1 x := x.(contents) := x.(contents).
+
+Ltac2 qux2 := ([1;2], true).
+
+Print Ltac2 qux0.
+Print Ltac2 qux1.
+Print Ltac2 qux2.
+
+Import Control.
+
+Ltac2 qux3 x := constr:(nat -> ltac2:(refine (fun () => hyp x))).
+
+Print Ltac2 qux3.
+
+Ltac2 Type rec nat := [ O | S (nat) ].
+
+Ltac2 message_of_nat n :=
+let rec aux n :=
+match n with
+| O => Message.of_string "O"
+| S n => Message.concat (Message.of_string "S") (aux n)
+end in aux n.
+
+Print Ltac2 message_of_nat.
+
+Ltac2 numgoals () :=
+  let r := { contents := O } in
+  enter (fun () => r.(contents) := S (r.(contents)));
+  r.(contents).
+
+Print Ltac2 numgoals.
+
+Goal True /\ False.
+Proof.
+let n := numgoals () in Message.print (message_of_nat n).
+refine (fun () => open_constr:((fun x => conj _ _) 0)); ().
+let n := numgoals () in Message.print (message_of_nat n).
+
+Fail (hyp ident:(x)).
+Fail (enter (fun () => hyp ident:(There_is_no_spoon); ())).
+
+enter (fun () => Message.print (Message.of_string "foo")).
+
+enter (fun () => Message.print (Message.of_constr (goal ()))).
+Fail enter (fun () => Message.print (Message.of_constr (qux3 ident:(x)))).
+enter (fun () => plus (fun () => constr:(_); ()) (fun _ => ())).
+plus
+  (fun () => enter (fun () => let x := ident:(foo) in let _ := hyp x in ())) (fun _ => Message.print (Message.of_string "failed")).
+let x := { contents := 0 } in
+let x := x.(contents) := x.(contents) in x.
+Abort.
+
+Ltac2 Type exn ::= [ Foo ].
+
+Goal True.
+Proof.
+plus (fun () => zero Foo) (fun _ => ()).
+Abort.
+
+Ltac2 Type exn ::= [ Bar (string) ].
+
+Goal True.
+Proof.
+Fail zero (Bar "lol").
+Abort.
+
+Ltac2 Notation "refine!" c(thunk(constr)) := refine c.
+
+Goal True.
+Proof.
+refine! I.
+Abort.
+
+Goal True.
+Proof.
+let x () := plus (fun () => 0) (fun _ => 1) in
+match case x with
+| Val x =>
+  match x with
+  | (x, k) => Message.print (Message.of_int (k Not_found))
+  end
+| Err x => Message.print (Message.of_string "Err")
+end.
+Abort.
+
+Goal (forall n : nat, n = 0 -> False) -> True.
+Proof.
+refine (fun () => '(fun H => _)).
+Std.case true (hyp @H, Std.ExplicitBindings [Std.NamedHyp @n, '0]).
+refine (fun () => 'eq_refl).
+Qed.
+
+Goal forall x, 1 + x = x + 1.
+Proof.
+refine (fun () => '(fun x => _)).
+Std.cbv {
+  Std.rBeta := true; Std.rMatch := true; Std.rFix := true; Std.rCofix := true;
+  Std.rZeta := true; Std.rDelta := true; Std.rConst := [];
+} { Std.on_hyps := None; Std.on_concl := Std.AllOccurrences }.
+Abort.
diff --git a/vendor/Ltac2/tests/tacticals.v b/vendor/Ltac2/tests/tacticals.v
new file mode 100644
index 0000000000..1a2fbcbb37
--- /dev/null
+++ b/vendor/Ltac2/tests/tacticals.v
@@ -0,0 +1,34 @@
+Require Import Ltac2.Ltac2.
+
+Import Ltac2.Notations.
+
+Goal True.
+Proof.
+Fail fail.
+Fail solve [ () ].
+try fail.
+repeat fail.
+repeat ().
+solve [ constructor ].
+Qed.
+
+Goal True.
+Proof.
+first [
+  Message.print (Message.of_string "Yay"); fail
+| constructor
+| Message.print (Message.of_string "I won't be printed")
+].
+Qed.
+
+Goal True /\ True.
+Proof.
+Fail split > [ split | |].
+split > [split | split].
+Qed.
+
+Goal True /\ (True -> True) /\ True.
+Proof.
+split > [ | split] > [split | .. | split].
+intros H; refine &H.
+Qed.
diff --git a/vendor/Ltac2/tests/typing.v b/vendor/Ltac2/tests/typing.v
new file mode 100644
index 0000000000..9f18292716
--- /dev/null
+++ b/vendor/Ltac2/tests/typing.v
@@ -0,0 +1,72 @@
+Require Import Ltac2.Ltac2.
+
+(** Ltac2 is typed à la ML. *)
+
+Ltac2 test0 n := Int.add n 1.
+
+Print Ltac2 test0.
+
+Ltac2 test1 () := test0 0.
+
+Print Ltac2 test1.
+
+Fail Ltac2 test2 () := test0 true.
+
+Fail Ltac2 test2 () := test0 0 0.
+
+Ltac2 test3 f x := x, (f x, x).
+
+Print Ltac2 test3.
+
+(** Polymorphism *)
+
+Ltac2 rec list_length l :=
+match l with
+| [] => 0
+| x :: l => Int.add 1 (list_length l)
+end.
+
+Print Ltac2 list_length.
+
+(** Pattern-matching *)
+
+Ltac2 ifb b f g := match b with
+| true => f ()
+| false => g ()
+end.
+
+Print Ltac2 ifb.
+
+Ltac2 if_not_found e f g := match e with
+| Not_found => f ()
+| _ => g ()
+end.
+
+Fail Ltac2 ifb' b f g := match b with
+| true => f ()
+end.
+
+Fail Ltac2 if_not_found' e f g := match e with
+| Not_found => f ()
+end.
+
+(** Reimplementing 'do'. Return value of the function useless. *)
+
+Ltac2 rec do n tac := match Int.equal n 0 with
+| true => ()
+| false => tac (); do (Int.sub n 1) tac
+end.
+
+Print Ltac2 do.
+
+(** Non-function pure values are OK. *)
+
+Ltac2 tuple0 := ([1; 2], true, (fun () => "yay")).
+
+Print Ltac2 tuple0.
+
+(** Impure values are not. *)
+
+Fail Ltac2 not_a_value := { contents := 0 }.
+Fail Ltac2 not_a_value := "nope".
+Fail Ltac2 not_a_value := list_length [].