diff --git a/src/How_to_Ltac2_contradiction.v b/src/How_to_Ltac2_contradiction.v
new file mode 100644
index 0000000..5d7a101
--- /dev/null
+++ b/src/How_to_Ltac2_contradiction.v
@@ -0,0 +1,826 @@
+(** * How to write a contradiction tactic with Ltac2
+
+  *** Authors
+  - Thomas Lamiaux
+
+  *** Summary
+
+  This tutorial explains how to write a variant of the [contradiction] tactic using Ltac2.
+  In particular, it showcases how to use [match! goal] and choose among [lazy_match!]
+  or [match!] and shows how to use quoting, and the Constr and Ind API to check properties on inductive types.
+
+  *** Table of content
+
+  - 1. Introduction
+  - 2. Matching the goal for [P] and [~P]
+    - 2.1 Choosing [lazy_match!], [match!] or [multi_match!]
+    - 2.2 Matching Syntactically or Semantically
+    - 2.3 Error messages
+  - 3. Using Constr.Unsafe and Ind API to Add Syntactic Checks
+    - 3.1 Checking for Empty and Singleton Types
+    - 3.2 Checking for Empty and Singleton Hypotheses
+  - 4. Putting it All Together
+
+  *** Prerequisites
+
+  Disclaimer:
+
+  Needed:
+  - Basic knowledge of Ltac2
+
+  Installation:
+  - Ltac2 and its core library are available by default with Rocq
+
+*)
+
+From Ltac2 Require Import Ltac2 Constr Printf.
+
+(** ** 1. Introduction
+
+    We write a variant of the [contradiction] tactic up to small differences.
+    The overall specification of [contradiction] is that it can take an argument or not:
+
+    If [contradiction] does not take an argument, then [contradiction]:
+    1. First introduces all the variables,
+    2. Tries to prove the goal by checking the hypotheses for:
+      - A pair of hypotheses [p : P] and [np : ~P], such that any goal can be
+        proven by [destruct (np p)]
+      - An hypothesis [x : T] where [T] is an inductive type without any constructor
+        like [False], in which case [destruct x] solves the current goal
+      - An hypothesis [nx : ~T] such that [T] is an inductive type with
+        one constructor without arguments, like [True] or [0 = 0];
+        in other words, such that [T] is provable by [constructor 1].
+
+    If [contradiction] takes an argument [t] then, the type of [t] must either be:
+    1. An empty inductive type like [False], in which case the goal is proven
+    2. Or a negation [~P], in which case:
+        - If there is a hypothesis of type [P] in the context, then the goal is proven;
+        - otherwise, the goal is replaced by [P].
+
+    In this how-to we will see how to write it using Ltac2.
+
+*)
+
+(** ** 2. Matching the goal for [P] and [~P]
+
+    *** 2.1 Choosing [lazy_match!], [match!] or [multi_match!]
+
+    To look up for a pair of hypotheses [P] and [~P], we need to match the goal.
+    There are three commands to match the goal that have different behaviour
+    regarding backtracking. The first step is to understand which one we want to use.
+
+    - [lazy_match! goal with] picks a branch, and sticks to it to even if the code
+      executed after picking this branch (the body of the branch) leads to a failure.
+      In practice, it is sufficient for all applications where matching the syntax
+      is enough and deterministic.
+
+    - [match! goal with] that picks the first branch that succeeds, but further backtracks
+      to its choice if the evaluation of its body fails to pick another matching branch,
+      potentially the same one if all the hypotheses have not been exhausted yet.
+      [match!] is useful as soon as matching the syntax is not enough, and we
+      need additional tests to see if we have picked the good hypotheses or not.
+
+    - [multi_match! goal with] that behaves like [match!] except that it will
+      further backtrack if its choice of a branch leads to a subsequent failure
+      when linked with another tactic.
+      [multi_match!] is meant to write tactics performing a choice, and that
+      we want to link with other tactics, like the [constructor] tactic.
+      The [contradiction] tactics is meant to solve goals with a simple enough
+      inconsistent context. It is not meant to be linked with other tactics.
+      Consequently, we have no use for [multimatch!] to implement [contradiction].
+
+    Choosing betwen [lazy_match!] and [match!] really depends if we need
+    more than a syntax check as we will see in the rest of this how-to guide.
+*)
+
+
+(** *** 2.2 Matching Syntactically or Semantically *)
+
+(** Whether we choose to use [lazy_match!] or [match!], there are different
+    ways to match for [P] and [~P]. We can match the syntax directly, or match
+    it semantically that is up to some reduction, conversion or unification.
+
+    This different options have different levels of expressiveness, allowing them
+    to match hypotheses to varying degrees. They also have different cost and side
+    effects, for instance, conversion does not unify evariables opposite to unify.
+
+    Understanding which strategy to choose is not easy. We will now discuss
+    the different options, and their pros and cons, before choosing one.
+
+
+    **** 2.2.1 Matching Syntactically
+
+    Except for non-linear matching, matching is by default syntactic.
+    That is, terms are matched and compared only up to α-conversion and evar expansion.
+    To match for [P] and [~P], we can use the pattern [p : ?t, np : ~(?t)].
+    In this pattern, [t] is non-linear so it will be matched up to conversion.
+    However, matching for a term of the form [~(_)] will be syntactically,
+    i.e. up to α-conversion.
+
+    If we have found hypotheses [P] and [~P], then we can prove [False].
+    Consequently, this is deterministic and we can use [lazy_match!] for it.
+*)
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  intros.
+  lazy_match! goal with
+  | [p : ?t, np : ~(?t) |- _ ] => printf "Hypotheses are %I,%I,%t" p np t
+  | [ |- _ ] => printf "There are no hypotheses left to try"; fail
+  end.
+Abort.
+
+(** Once we have found [P] and [~P], we want to prove [False] using the usual
+    [destruct] tactic that expects a Rocq term, that is we want to write [destuct (np p)].
+    However, this is not possible as though, as [p : ident] and [np : ident] are
+    identifiers, i.e. the name of the hypotheses [P] and [~P], wheras [destruct X]
+    expects [X] to be a Rocq term.
+
+    To get the terms associated to [p] and [np], we must use [Control.hyp : ident -> contr],
+    which transforms an [ident] corresponding to an hypothesis into a Rocq term
+    we can manipulate in Ltac2, that is, into an object of type [constr].
+    If there are no such hypotheses then it raises an error.
+    For [p] and [np], this gives us:
+
+    [[  let p := Control.hyp p in
+        let np := Control.hyp np in
+        ...
+    ]]
+
+    Once, we have gotten the term associated to the hypotheses with [Control.hyp],
+    we must go back to Rocq's world to be able to use [destruct].
+    We do so with [$], which leads to:
+
+    [[
+      let p := Control.hyp p in
+      let np := Control.hyp np in
+      destruct ($np $p)
+    ]]
+
+    Notation, to do [Control.hyp] and [$] at once is only available in Rocq 9.1 or above.
+
+    This leads us to the following script:
+*)
+
+Ltac2 match_PnP_syntax () :=
+  lazy_match! goal with
+  | [p : ?t, np : ~(?t) |- _ ] =>
+        printf "Hypotheses are %I,%I,%t" p np t;
+        let p := Control.hyp p in
+        let np := Control.hyp np in
+        destruct ($np $p)
+  | [ |- _ ] => printf "There are no hypotheses left to try"; fail
+  end.
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  intros. match_PnP_syntax ().
+Qed.
+
+Goal forall P, P -> (P -> nat) -> False.
+  intros. Fail match_PnP_syntax ().
+Abort.
+
+(** It has the advantage to be fast but the downside is that it will not match
+    [?t -> False], even though it is convertible to [~(?t)], as [~(_)] is
+    match syntactically.
+    It is not what we want for a [contradiction] tactic.
+*)
+
+Goal forall P, P -> (P -> False) -> False.
+  intros. Fail match_PnP_syntax ().
+Abort.
+
+(** To deal with [?t -> False], we could be tempted to add an extra-pattern in
+    the definition, but this would not scale as any variations around [~] would fail.
+*)
+
+Goal forall P, P -> ((fun _ => ~P) 0) -> False.
+  intros. Fail match_PnP_syntax ().
+Abort.
+
+(** Checking terms up to syntax is not a good notion of equality in type theory.
+    For instance, [4 + 1] is not syntactically equal to [5].
+    What we really want here is to compare type semantically, i.e. up to
+    some reduction, conversion or unification.
+*)
+
+(** Note, however, that it would match [~((fun _ => P) 0)] as [t] in [~t] is
+    matched up to conversion.
+*)
+
+Goal forall P, P -> ~ ((fun _ => P) 0) -> False.
+  intros. match_PnP_syntax ().
+Abort.
+
+(** **** 2.2.2 Matching up to Unification
+
+    Before considering finer ways to compare terms semantically, let us first
+    consider how to match terms up to unification as it is what comes up
+    first to mind when trying to write meta-programming.
+
+    To match semantically, we must match for a pair of hypotheses
+    [p : ?t1, np : ?t2 |- _], then check that [t2] is of the form [t1 -> False].
+    Something fundamental to understand, here, is that with this approach the
+    syntax check is no longer sufficient to be able to prove [False], as we match
+    for any pair of hypotheses then check we have picked the good ones.
+    We hence need to switch from [lazy_match!] to [match!] to be able to
+    backtrack and try the next hypotheses, if we have picked the wrong ones.
+
+    To unify the types, we can exploit that tactics do unification.
+    For instance, we can ensure that [t2] is of the shape [t1 -> X] by applying
+    [$np] to [$p]; i.e. [$np $p], as otherwise it would be ill-typed.
+    We also need to ensure that [X] is [False], otherwise, [destruct ($np $p)]
+    could do pattern matching on [nat] which would not solve the goal.
+    We can ensure that it does solve the goal by wrapping it in [solve].
+    However, it is not an efficient solution, as we would still do [destruct] for
+    every pair of hypotheses until we found one that works, which can be costly.
+    A better solution, is to use a type annotation [$np $p :> False] to force the
+    type of [$np $p] to be [False].
+
+    This leads to the script:
+*)
+
+Ltac2 match_PnP_unification_v1 () :=
+  match! goal with
+  | [p : ?t1, np : ?t2 |- _ ] =>
+        printf "Hypotheses are %I : %t, and %I : %t" p t1 np t2;
+        let p := Control.hyp p in
+        let np := Control.hyp np in
+        destruct ($np $p :> False)
+  | [ |- _ ] => printf "There are no hypotheses left to try"; fail
+  end.
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  intros. match_PnP_unification_v1 ().
+Qed.
+
+Goal forall P, P -> (P -> nat) -> False.
+  intros. Fail match_PnP_unification_v1 ().
+Abort.
+
+Goal forall P, P -> (P -> False) -> False.
+  intros. match_PnP_unification_v1 ().
+Qed.
+
+Goal forall P, P -> ((fun _ => ~P) 0) -> False.
+  intros. match_PnP_unification_v1 ().
+Qed.
+
+(** While this technically works, a better and more principled approach is to
+    directly use the primitive [Std.unify : constr -> constr -> unit] that
+    that unifies two terms, and raises an exception if it is not possible.
+
+    With this approach, there are much less chances to make an error,
+    like misunderstanding how unification is done by the tactics, or
+    forgetting the type annotation [:> False].
+
+    Moreover, it scales much better. Conversion is only available for
+    Rocq 9.1 and later versions, so we will not utilize it in this how-to guide.
+    However, if it were available, we could essentially replace [Std.unify]
+    with [Std.conversion] to obtain the alternative version.
+    One could even consider parametrising the code by a check that could later
+    be instantiated with unification, conversion or some syntax check up to
+    reduction, like to the head normal form.
+*)
+
+Ltac2 match_PnP_unification_v2 () :=
+  match! goal with
+  | [p : ?t1, np : ?t2 |- _ ] =>
+        printf "Hypotheses are %I : %t, and %I : %t" p t1 np t2;
+        Std.unify t2 '($t1 -> False);
+        printf "Unification Worked!";
+        let p := Control.hyp p in
+        let np := Control.hyp np in
+        destruct ($np $p)
+  | [ |- _ ] => printf "There are no hypotheses left to try"; fail
+  end.
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  intros. match_PnP_unification_v2 ().
+Qed.
+
+Goal forall P, P -> (P -> nat) -> False.
+  intros. Fail match_PnP_unification_v2 ().
+Abort.
+
+Goal forall P, P -> (P -> False) -> False.
+  intros. match_PnP_unification_v2 ().
+Qed.
+
+Goal forall P, P -> ((fun _ => ~P) 0) -> False.
+  intros. match_PnP_unification_v2 ().
+Qed.
+
+(** An issue with unification is that it can unify evariables.
+    For instance [match_PnP_unification_v2] can solve the following goal
+    which is not the case for the usual [contradiction] tactic.
+*)
+
+Goal forall P Q, P -> ~Q -> False.
+  intros. eassert (X4 : _) by admit.
+  match_PnP_unification_v2 ().
+Abort.
+
+(** This is costly, but also not a very good practice for automation tactics
+    which should not unify evariables behind the scene as it can
+    unify them in an unexpected way getting the users stuck later.
+    Users should have control on whether evariables are unified or not, hence
+    the different e-variants like [assumption] and [eassumption].
+*)
+
+(** **** 2.2.3 Matching up to Reduction
+
+    To have finer control on what happens and reduce the cost of unification,
+    we can instead reduce our types to a head normal form to check it is of the
+    form [X -> Y] as [->] is an infix notation, (it should be seen as [-> X Y]).
+    We can then check that [X] is [t1], and [Y] is [False].
+
+    To reduce terms, there are many primitives in [Std]. We want to reduce to the
+    head normal form so we can use directly [Std.eval_hnf : constr -> constr].
+    We can then match the head with [lazy_match!] with the pattern [?x -> ?y].
+    We use [lazy_match!] as this is deterministic, either our term is a product
+    or it is not.
+
+  [[
+    match! goal with
+    | [p : ?t1, np : ?t2 |- _ ] =>
+          let t2' := Std.eval_hnf t2 in
+          lazy_match! t2' with
+          | ?x -> ?y => printf "(%I : %t) is a product %t -> %t" np t2 x y;
+          | _ => printf "(%I : %t) is not product" np t2;
+          end
+    | [ |- _ ] => printf "There are no hypotheses left to try"; fail
+  ]]
+
+    We then have to compare [X] with [t1], and [Y] with [False]. We would like to
+    compare terms up to conversion as it is reasonably inexpensive, but still
+    very expressive. Unfortunately, there is no primitive for it at the moment.
+
+    Consequently, we compare them up to syntactic equality which is still very
+    expressive when combined with reduction using [Constr.equal : term -> term -> bool].
+    This gives us the following script to which we add some printing functions
+    to see what is going on.
+*)
+
+Ltac2 match_PnP_unification_v3 () :=
+  match! goal with
+  | [p : ?t1, np : ?t2 |- _ ] =>
+        printf "Hypotheses are %I : %t, and %I : %t" p t1 np t2;
+        lazy_match! (Std.eval_hnf t2) with
+        | ?x -> ?y =>
+            printf "(%I : %t) is a product %t -> %t" np t2 x y;
+            if Bool.and (Constr.equal (Std.eval_hnf x) t1)
+                        (Constr.equal (Std.eval_hnf y) 'False)
+            then printf "(%I : %t) is a contradiction of (%I : %t)" np t2 p t1;
+                 let p := Control.hyp p in
+                 let np := Control.hyp np in
+                 destruct ($np $p)
+            else (printf "(%I : %t) is not a contradiction of (%I : %t)" np t2 p t1;
+                  printf "----- Backtracking -----"; fail)
+        | _ => printf "(%I : %t) is not product" np t2;
+               printf "----- Backtracking -----"; fail
+        end
+  | [ |- _ ] => printf "There are no hypotheses left to try"; fail
+  end.
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  intros. match_PnP_unification_v3 ().
+Qed.
+
+Goal forall P, P -> (P -> nat) -> False.
+  intros. Fail match_PnP_unification_v3 ().
+Abort.
+
+Goal forall P, P -> (P -> False) -> False.
+  intros. match_PnP_unification_v3 ().
+Qed.
+
+Goal forall P, P -> ((fun _ => ~P) 0) -> False.
+  intros. match_PnP_unification_v3 ().
+Qed.
+
+(** However, this now fails as evariables are no longer unified. *)
+
+Goal forall P Q, P -> ~Q -> False.
+  intros. eassert (X4 : _) by admit.
+  Fail match_PnP_unification_v3 ().
+Abort.
+
+(** **** 2.2.4 Optimisation
+
+    Using reduction already provides us with a fine control over what is going on
+    but is still a bit inefficient as we try to compare every pair of hypotheses.
+    Instead, we can look for a negation [~P], and only if found check
+    for an hypothesis [P]. This basically amounts to spliting the match in
+    two parts. As it can be seen, it matches much fewer hypotheses in case of failure.
+*)
+
+Ltac2 match_PnP_unification_v4 () :=
+  match! goal with
+  | [np : ?t2 |- _ ] =>
+      printf "Hypothesis is %I : %t" np t2;
+      let np := Control.hyp np in
+      (* Check [t2] is a negation ~P *)
+      lazy_match! (Std.eval_hnf t2) with
+      | ?x -> ?y =>
+        if Constr.equal (Std.eval_hnf y) 'False then
+          printf "%t is a negation %t -> %t" t2 x y;
+          printf "Search for %t:" x;
+          printf "    ------------------------";
+          (* Check for an hypothesis P *)
+          match! goal with
+          | [p : ?t1 |- _ ] =>
+            printf "    Hypothesis is %I : %t" p t1;
+            if Constr.equal (Std.eval_hnf x) t1
+            then printf "    %t is a contradiction of %t" t2 t1;
+                 let p := Control.hyp p in destruct ($np $p)
+            else (printf "    ----- Backtracking -----"; fail)
+          | [ |- _ ] => printf "    There are no hypotheses left to try";
+                        printf "----- Backtracking -----"; fail
+          end
+        else ( printf "%t is not a negation" t2;
+               printf "----- Backtracking -----"; fail)
+      | _ => printf "%t is not a negation" t2;
+             printf "----- Backtracking -----"; fail
+      end
+  | [ |- _ ] => printf "Failure: There are no hypotheses left to try"; fail
+  end.
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  intros. match_PnP_unification_v4 ().
+Qed.
+
+Goal forall P, P -> (P -> nat) -> False.
+  intros. Fail match_PnP_unification_v4 ().
+Abort.
+
+Goal forall P, P -> (P -> False) -> False.
+  intros. match_PnP_unification_v4 ().
+Qed.
+
+Goal forall P, P -> ((fun _ => ~P) 0) -> False.
+  intros. match_PnP_unification_v4 ().
+Qed.
+
+Goal forall P Q, P -> ~Q -> False.
+  intros. eassert (X4 : _) by admit.
+  Fail match_PnP_unification_v4 ().
+Abort.
+
+(** *** 2.3 Error Messages
+
+  So far, we have been using [fail] to trigger failure, which returns
+  the error message [Tactic_failure None].
+
+  We can be finer using the primitive [Control.zero : exn -> 'a] to raise an error.
+  We can then raise a custom error message using [Tactic_failure : message option -> exn]
+  that raises an error for any given message.
+  We can then write complex error message using [fprintf] that behaves as [printf]
+  excepts that it returns a [message] rather than printing it.
+*)
+
+Goal forall P, P -> (P -> nat) -> False.
+  Fail match! goal with
+  | [ |- _ ] => Control.zero (Tactic_failure (Some (fprintf "No such contradiction")))
+  end.
+Abort.
+
+(** The error type [exn] is an open type, which mean we can add a constructor to it,
+    i.e. a new exception, at any point.
+    We can hence create a new exception just for [contradiction].
+*)
+
+Ltac2 Type exn ::= [ Contradiction_Failed (message option) ].
+
+Goal forall P, P -> (P -> nat) -> False.
+  Fail match! goal with
+  | [ |- _ ] => Control.zero (Contradiction_Failed (Some (fprintf "No such contradiction")))
+  end.
+Abort.
+
+
+(** ** 3. Using Constr.Unsafe and Ind API to Add Syntactic Checks
+
+    We need to check for hypotheses that are either empty like [False], or
+    of form [~t] where [t] is an inductive type with one constructor without
+    arguments like [nat] or [0 = 0] that we can prove with [constructor 1].
+
+    We can do so very directly by trying to solve the goal assuming we have
+    found the good hypotheses wrapping it in [solve] to ensure that it works.
+    In this case, for [p : t] and [np : ~t] that would mean doing
+    [solve [destruct $p]] and [destruct ($np ltac2:(constructor 1))].
+    However, that would be very inefficient as we would [destruct] any hypothesis, which can be expensive.
+
+    A better approach is to add a syntax check that verifies that [t] is of the
+    appropriate form. It is much cheaper as it is basically matching syntax.
+    We can do so by using the API [Constr.Unsafe] that enables to access the
+    internal syntax of Rocq terms, and [Ind] to access inductive types.
+
+    The API "unsafe" is named this way because as soon as you start manipulating
+    internal syntax, there is no longer any guarantee you create well-scoped terms.
+    Here, we will only use it to match the syntax so there is nothing to worry about.
+*)
+
+(** *** 3.1 Checking for Empty and Singleton Types
+
+    In both cases, the first step is to check if the term is an inductive type.
+    Internally, a type like [list A] is represented as [App (Ind ind u) args]
+    where [ind] is the name of the inductive and the position of the block,
+    and [u] represents universe constraints.
+    Consequently, given a [t : constr] we need to decompose the application
+    [App x args], then match [x] for [Ind ind u].
+
+    This can be done using [Unsafe.kind : constr -> kind] which converts a
+    [constr] to a shallow embedding of the internal syntax, which is defined
+    as a Ltac2 inductive type [kind].
+    [kind] is a shallow embedding which means a [constr] is not fully
+    converted to a representation of the internal syntax, only its head.
+    For example, the type of [Unsafe.App] is [constr -> constr array -> kind].
+    That is, [u] and [v] in [Unsafe.App u v] remain regular [constr] elements
+    and are not recursively converted to [kind], which characterizes it as shallow.
+    In contrast, if we had a deep embedding, the arguments of [Unsafe.App] would be
+    recursively converted to [kind], resulting in the type [kind -> kind array -> kind].
+    The reason for using a shallow embedding is that it is much faster than fully
+    converting terms to the internal syntax, yet sufficient for most applications.
+
+    Let us first write a function [decompose_app] that translates a [constr] to
+    [kind], then match it for [Unsafe.App] and returns the arguments.
+    It is already available starting Rocq 9.1, but it still is good to recode it.
+
+    There are two things to understand here:
+    - 1. We match [kind] using [match] and not with [match!] as [kind] is an
+         inductive type of Ltac2. [match!] is to match [constr] and goals.
+    - 2. We really need the shallow embedding: we cannot match the type of a
+         term as we did for [X -> Y]. Indeed, we can match [X -> Y] with [match!]
+         as we know there are exactly 2 arguments, so the syntax is fully specified.
+         In constrasts, an application like an inductive type could have arbitrary
+         many arguments, and we can hence not match it with [match!]
+*)
+
+Ltac2 decompose_app (t : constr) :=
+  match Unsafe.kind t with
+    | Unsafe.App f cl => (f, cl)
+    | _ => (t,[| |])
+  end.
+
+(** Getting the inductive data associated to an inductive block is similar.
+    We first use [decompose_app] to recover the left side of the application,
+    we then convert to the syntax to check if it is an inductive, in which case
+    we recover the inductive definition with [Ind.data : inductive -> data].
+
+    A subtlety to understand is that [Unsafe.kind] converts the syntax without
+    reducing terms. So if we want [(fun _ => True) 0] to be considered as an
+    inductive, we need to reduce it first to a head normal form with
+    [Std.eval_hnf : constr -> constr].
+ *)
+
+Import Ind.
+
+Ltac2 get_inductive_body (t : constr) : data option :=
+  let (x, _) := decompose_app (Std.eval_hnf t) in
+  match Unsafe.kind (Std.eval_hnf x) with
+  | (Unsafe.Ind ind _) => Some (Ind.data ind)
+  | _ => None
+  end.
+
+(** We are ready to check if a type is empty or not, which is now fairly easy.
+    Given the definition of an inductive type, it suffices to get the number
+    of constructor with [nconstructors : data -> int], and check it is zero.
+*)
+
+Ltac2 is_empty_inductive (t : constr) : bool :=
+ match get_inductive_body t with
+ | Some ind_body => Int.equal (Ind.nconstructors ind_body) 0
+ | None => false
+ end.
+
+(** We can check an inductive type is a singleton similarly, except to one small issue.
+    The primitive to access the arguments of a constructor is only available in
+    Rocq 9.1 or above. So for now, we will hence only check that it has only one constructor.
+    Though this is not perfect and forces us to wrap [destruct ($np ltac2:(constructor 1)]
+    in [solve], it still rules out most inductives like [nat].
+*)
+
+Ltac2 is_singleton_type (t : constr) : bool :=
+  match get_inductive_body t with
+  | Some ind_body => Int.equal (Ind.nconstructors ind_body) 1
+  | None => false
+  end.
+
+(** *** 3.2 Checking for Empty and Singleton Hypotheses
+
+    Writing a tactic to check for empty hypothesis is now fairly easy.
+    We just match the goal using [match!] as the syntax check is not complete,
+    then check if it is empty, and if it is, prove the goal with [destruct $p].
+*)
+
+Ltac2 match_P_empty () :=
+  match! goal with
+  | [ p : ?t |- _ ] =>
+        let p := Control.hyp p in
+        if is_empty_inductive t then destruct $p else fail
+  | [ |- _ ] => Control.zero (Contradiction_Failed (Some (fprintf "No such contradiction")))
+  end.
+
+Goal False -> False.
+  intros. match_P_empty ().
+Qed.
+
+Goal True -> False.
+  intros. Fail match_P_empty ().
+Abort.
+
+(** Checking for the negation of an inductive type is a little bit more involved
+    as we need to check the type of [?] is of the form [?X -> False].
+    We can do so by creating a fresh evariable of type [Type] with
+    [open_constr:(u :> Type)] then using [Std.unifiy]:
+*)
+
+Ltac2 match_nP_singleton () :=
+  match! goal with
+  | [ np : ?t2 |- _ ] =>
+      let np := Control.hyp np in
+      lazy_match! (Std.eval_hnf t2) with
+      | ?x -> ?y =>
+        if Bool.and (is_singleton_type x) (Constr.equal (Std.eval_hnf y) 'False)
+        then solve [destruct ($np ltac2:(constructor 1))]
+        else printf "%t is not a singeleton or %t is not False" x y ; fail
+      | _ => printf "%t is not product" t2; fail
+      end
+  | [ |- _ ] => Control.zero (Contradiction_Failed (Some (fprintf "No such contradiction")))
+  end.
+
+Goal ~True -> False.
+  intros. match_nP_singleton ().
+Qed.
+
+Goal ~(0 = 0) -> False.
+  intros. match_nP_singleton ().
+Qed.
+
+Goal ~(0 = 1) -> False.
+  intros. Fail match_nP_singleton ().
+Abort.
+
+(** ** 4. Putting it All Together *)
+
+(** It took a few explanations, but in the end the code of [contradiction_empty]
+    is rather short using Ltac2.
+
+    To be efficient, we first perform the syntax check as it is very cheap.
+    We hence first check for an empty hypotheses, then if it is a negation,
+    in particular of a singletion inductive type. If it is none of these,
+    check for [P] and [~P] which we perform last in order not to check
+    the whole context for nothing.
+*)
+
+Ltac2 contradiction_empty () :=
+  intros;
+  match! goal with
+  | [np : ?t2 |- _ ] =>
+      let np := Control.hyp np in
+      (* Check if [t2] is empty  *)
+      if is_empty_inductive t2 then destruct $np else
+      (* If it is not, check if [t2] is a negation ~P *)
+      lazy_match! (Std.eval_hnf t2) with
+      | ?x -> ?y =>
+          if Constr.equal (Std.eval_hnf y) 'False then
+            (* If so check if [x] is empty *)
+            if is_singleton_type x
+            then solve [destruct ($np ltac2:(constructor 1))]
+            (* If not, check for an hypothesis P *)
+            else (match! goal with
+              | [p : ?t1 |- _ ] =>
+                if Constr.equal (Std.eval_hnf x) t1
+                then let p := Control.hyp p in destruct ($np $p)
+                else fail
+              | [ |- _ ] => fail
+            end)
+          else fail
+      | _ => fail
+      end
+  | [ |- _ ] => fail
+  end.
+
+(** We also need to write a [contradiction] when it takes an argument. *)
+
+Ltac2 contradiction_arg (t : constr) :=
+  lazy_match! (Std.eval_hnf (type t)) with
+  | ?x -> ?y =>
+      if Constr.equal (Std.eval_hnf y) 'False
+      then match! goal with
+        | [p : ?t1 |- _ ] =>
+            if Constr.equal (Std.eval_hnf x) t1
+            then let p := Control.hyp p in destruct ($t $p)
+            else fail
+        | [ |- _ ] => assert (f : False) > [apply $t | destruct f]
+        end
+      else fail
+  | _ => Control.zero (Contradiction_Failed (Some (fprintf "%t is not a negation" t)))
+  end.
+
+Goal forall P, P -> ~P -> 0 = 1.
+  intros P p np. contradiction_arg 'np.
+Qed.
+
+Goal forall P, ~P -> 0 = 1.
+  intros P np. contradiction_arg 'np.
+Abort.
+
+Goal forall P, P -> 0 = 1.
+  intros P p. Fail contradiction_arg 'p.
+Abort.
+
+(** Finally, we define a wrapper for it :  *)
+
+Ltac2 contradiction0 (t : constr option) :=
+  match t with
+  | None => contradiction_empty ()
+  | Some x => contradiction_arg x
+  end.
+
+(** We can now use [contradiction0] directly writing [None] and [Some], and
+    the quoting constructor by hand.
+*)
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  contradiction0 None.
+Qed.
+
+Goal forall P, P -> ~P -> 0 = 1.
+  intros P p np. contradiction0 (Some 'np).
+Qed.
+
+(** Alternatively, we can define a notation to do deal insert [None], [Some] and
+    the quoting for us, but be aware it may complicate parsing.
+*)
+
+Ltac2 Notation "contradiction" t(opt(constr)) := contradiction0 t.
+
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  contradiction.
+Qed.
+
+Goal forall P, P -> ~P -> 0 = 1.
+  intros P p np. contradiction np.
+Qed.
+
+(** Finally, just to be sure everything is alright, let us check [contradiction]
+    on all the examples we have seen so far.
+*)
+
+(* pairs of hypotheses *)
+Goal forall P Q, P -> ~Q -> ~P -> False.
+  contradiction.
+Qed.
+
+Goal forall P, P -> (P -> nat) -> False.
+  Fail contradiction.
+Abort.
+
+Goal forall P, P -> (P -> False) -> False.
+  contradiction.
+Qed.
+
+Goal forall P, P -> ((fun _ => ~P) 0) -> False.
+  contradiction.
+Qed.
+
+Goal forall P Q, P -> ~Q -> False.
+  intros. eassert (X4 : _) by admit.
+  Fail contradiction.
+Abort.
+
+(* empty hypotheses *)
+Goal False -> False.
+  contradiction.
+Qed.
+
+Goal True -> False.
+  Fail contradiction.
+Abort.
+
+(* Negation of a singleton *)
+Goal ~True -> False.
+  contradiction.
+Qed.
+
+Goal ~(0 = 0) -> False.
+  contradiction.
+Qed.
+
+Goal ~(0 = 1) -> False.
+  Fail contradiction.
+Abort.
+
+(* negation given as an argument *)
+Goal forall P, P -> ~P -> 0 = 1.
+  intros P p np. contradiction np.
+Qed.
+
+Goal forall P, ~P -> 0 = 1.
+  intros P np. contradiction np.
+Abort.
+
+Goal forall P, P -> 0 = 1.
+  intros P p. Fail contradiction p.
+Abort.
\ No newline at end of file
diff --git a/src/Tutorial_Ltac2_matching_terms_and_goals.v b/src/Tutorial_Ltac2_matching_terms_and_goals.v
new file mode 100644
index 0000000..77406f2
--- /dev/null
+++ b/src/Tutorial_Ltac2_matching_terms_and_goals.v
@@ -0,0 +1,639 @@
+(** * Tutorial Ltac2 : Matching Terms and Goals
+
+  *** Authors
+  - Thomas Lamiaux
+
+  *** Summary
+
+  Ltac2 has native support to match the structure of terms, and of the goal,
+  making it easy to build decision procedures or solvers.
+  There are three primitives to match terms or goals [lazy_match!], [match!],
+  and [multi_match!], which only differ by their backtracking abilities.
+  (Not to confuse with [match] which is for Ltac2 inductive types.)
+  Consequently, we first explain how matching terms and goals work using
+  [lazy_match!], then discuss the backtracking differences in a third section.
+
+  *** Table of content
+
+  - 1. Matching Terms
+    - 1.1 Basics
+    - 1.2 Non-Linear Matching
+  - 2Matching Goals
+    - 1.1 Basics
+    - 1.2 Non-Linear Matching
+  - 3. Backtracking and [lazy_match!], [match!], [multi_match!]
+    - 3.1 [lazy_match!]
+    - 3.2 [match!]
+    - 3.3 [multi_match!]
+
+  *** Prerequisites
+
+  Disclaimer:
+
+  Needed:
+  - Basic knowledge of Ltac2
+
+  Installation:
+  - Ltac2 and its core library are available by default with Rocq.
+*)
+
+(** Let us first import Ltac2, and write a small function printing the goal under focus. *)
+From Ltac2 Require Import Ltac2 Printf.
+Import Bool.BoolNotations.
+
+Ltac2 print_goals0 () :=
+  Control.enter (fun () =>
+  match! goal with
+  [ |- ?t] => printf "the goal is %t" t
+  end
+  ).
+
+Ltac2 Notation print_goals := print_goals0 ().
+
+(** ** 1 Matching terms
+
+    *** 1.1 Basics
+
+    Ltac2 has primitives to match a term to inspect its shape, for instance,
+    if it is a function or a function type.
+    This enables to perform different actions depending on the shape of the term.
+
+    To match a term, the syntax is [lazy_match! t with] with one clause of
+    the form [ ... => ...] per pattern to match.
+    As an example, let's write a small function proving the goal provided
+    it is given an argument of type [True -> ... True -> False].
+
+    We write a recursive function that matches the type of [t] obtained with
+    [Constr.type : constr -> constr] against [False] and [True -> _].
+    In the first case, we prove the goal with [destruct $t], in the second
+    case we recursively attempt to solve the goal with [triv '($t I)] by
+    applying [t] to the only inhabitant of [True], [I : True].
+*)
+
+Ltac2 rec triv (t : constr) :=
+  lazy_match! Constr.type t with
+  | False => destruct $t
+  | True -> _ => triv '($t I)
+  end.
+
+Goal False -> True.
+  intros H. triv 'H.
+Abort.
+
+Goal (True -> True -> True -> False) -> True.
+  intros H. triv 'H.
+Abort.
+
+Goal True -> True.
+  intros H. Fail triv 'H.
+Abort.
+
+(** As in Rocq, the default pattern is a wildcard [_], that will match anything.
+    It is practical to do something specific if the term matched is of any other
+    shape than the one matched.
+    For instance, we can use it to return a more specific error than
+    [Match_failure] by defining [err_triv] to return if it fails.
+*)
+
+Ltac2 err_triv t := Control.zero (Tactic_failure (Some (
+    fprintf "%t is not of the form True -> ... -> True -> False" t
+  ))).
+
+Ltac2 rec triv_err (t : constr) :=
+  let ty := Constr.type t in
+  printf "the type under consideration is %t" ty;
+  lazy_match! ty with
+  | False => destruct $t
+  | True -> _ => triv_err '($t I)
+  | _ => err_triv ty
+  end.
+
+Goal True -> True.
+  intros H. Fail triv_err 'H.
+Abort.
+
+(** In some cases, we do not want to merely match the shape of a term [t],
+    but also to recover a part of this subterm to perform more actions on it.
+    This can be done using variables which must be written [?x].
+    In such cases, [x] is of type [constr], the type of Rocq terms in Ltac2.
+    This is normal as [x] corresponds to a subterm of [t].
+
+    Note that as in Ocaml, variable names cannot start with an upper case letter as this
+    is reserved for constructors of inductive types.
+
+    As an example consider writing a boolean (in Ltac2, not in Rocq) test to check if a type is a
+    proposition written out of [True], [False], [~] ,[/\] ,[\/].
+    To check a term is a proposition, we need to match it to inspect its head symbol,
+    and if it is one of the allowed one check its subterms also are propositions.
+    Consequently, we need to remember subterms, and to match [/\] we need to
+    use the pattern [?a /\ ?b]. This gives the following recursive function:
+*)
+
+Ltac2 rec is_proposition (t : constr) :=
+  lazy_match! t with
+  | True => true
+  | False => true
+  | ?a /\ ?b => is_proposition a && is_proposition b
+  | ?a \/ ?b => is_proposition a && is_proposition b
+  | _ => false
+  end.
+
+(** To test it, lets us write a small printing function. *)
+Ltac2 check_is_proposition (t : constr) :=
+  if is_proposition t
+  then printf "%t is a proposition" t
+  else printf "%t is not a proposition" t.
+
+Goal (True \/ (True /\ False)) -> nat -> True.
+  intros H1 H2.
+  check_is_proposition (Constr.type 'H1).
+  check_is_proposition (Constr.type 'H2).
+Abort.
+
+
+(** ** 1.2 Non-Linear Matching
+
+    Matching of syntax is by default syntactic. It means terms are only inspected
+    to be of the appropriate shape up to α-conversion and expansion of evars.
+
+    For instance, [fun x => x] and [fun y => y] are equal syntactically as they
+    only differ by their names of bound variables (α-conversion), but [1 + 4]
+    and [5] are not equal syntactically as they only are equal up to reduction.
+    As a consequence, a small variation around a term that would require a
+    reduction step like [(fun _ => False) 0] will not be matched by [False].
+*)
+
+Goal ((fun _ => False) 0) -> False.
+  intros H. Fail triv_err 'H.
+Abort.
+
+(** In Ltac2, it is up to the users to reduce the terms appropriately before matching them.
+    In most cases, we match the syntax to find what is the head symbol [False]
+    or [->], in which case it suffices to compute the head normal form (hnf)
+    with [Std.eval_hnf : constr -> constr].
+    With extra-printing to show the difference before and after [eval_hnf],
+    this gives us this barely different version of [triv_err].
+*)
+
+Ltac2 rec triv_hnf (t : constr) :=
+  let ty := Constr.type t in
+  printf "the type under consideration is %t" ty;
+  let ty_hnf := Std.eval_hnf ty in
+  printf "the hnf type under consideration is %t" ty_hnf;
+  lazy_match! ty_hnf with
+  | False => destruct $t
+  | True -> _ => triv_hnf '($t I)
+  | _ => err_triv ty_hnf
+  end.
+
+Goal (True -> ((fun _ => False) 0)) -> True.
+  intros H. triv_hnf 'H.
+Abort.
+
+Goal (True -> (((fun _ => True) 0) -> True -> False)) -> True.
+  intros H. triv_hnf 'H.
+Abort.
+
+(** The advantage of this approach is that the default is fast and predictable,
+    and full control is left to the user to compare terms up to the notion of
+    their choosing like up to head-normal form, or up to unification.
+
+    This explains how syntax is matched but not how a pattern is matched when a
+    variable [?x] appears more than once in a pattern, like [?x = ?x].
+    Such patterns are called non-linear, and are matched up to conversion.
+    The reason is that we expect the subterms matched to be the same,
+    which in type theory naturally corresponds to conversion.
+*)
+
+Ltac2 is_refl_eq (t : constr) :=
+  lazy_match! t with
+  | ?x = ?x => printf "it is a reflexive equality"
+  | _ => printf "it is not a reflexive equality"
+  end.
+
+Goal (1 = 1) -> False.
+  intros H. is_refl_eq (Constr.type 'H).
+Abort.
+
+(** Ltac2 naturally detects when a variable is not used after the matching pattern,
+    in which case it triggers a warning.
+    This warning will be triggered for non-linear variables, if they are only used
+    to constrain the shape of the term matched, like in [is_refl_eq], but no further.
+    In this case, the warning can be easily disable by naming unused variables
+    starting with [?_] rather than with [?].
+    For instance, by matching for [?_x = ?_x] rather than [?x = ?x] is [is_refl_eq].
+*)
+
+Ltac2 is_refl_eq' (t : constr) :=
+  lazy_match! t with
+  | ?_x = ?_x => printf "it is a reflexive equality"
+  | _ => printf "it is not a reflexive equality"
+  end.
+
+Goal (1 = 1) -> False.
+  intros H. is_refl_eq (Constr.type 'H).
+Abort.
+
+(** 2. Matching Goals
+
+    2.1 Basics
+
+    Ltac2 also offers the possibility to match the goals to inspect the form the goal
+    to prove, and/or the existence of particular hypotheses like a proof of [False].
+    The syntax to match goals is a bit different from matching terms.
+    In this case, the patterns are of the form:
+
+        [[ [ x1 : t1, ..., xn : tn |- g ] => ... ]]
+
+    where:
+    - [x1] ... [xn] are [ident], i.e. Ltac2 values corresponding to the names
+      of the hypotheses. Opposite to variables, they should not start with [?].
+    - [t1] ... [tn] are the types of the hypotheses, and [g] the type of the goal
+      we want to prove. All are of type [constr], the type of Rocq terms in Ltac2.
+    - As usual [ident] --- [x1], ..., [xn] --- and any variables that could appear
+      in [t1], ..., [tn], and [g], cannot start with an upper case letter as
+      it is reserved for constructors.
+
+    Such a pattern will match the conclusion of the goal of type [G], and such that
+    can be found [n] different hypotheses of types [T1], ..., [Tn].
+    Each clause must match a different hypothesis for the pattern to succeed.
+    Consequently, there must be at least [n] different hypotheses / assumptions
+    in the context for such a branch to have a chance to succeed.
+    Moreover, the fallback wildcard pattern [_] we used to match terms is
+    now [ |- _] as this matches any goals.
+
+    As an example, let us write a small function starting with [lazy_match! goal with]
+    to inspect if the conlusion of the goal is either [_ /\ _] or [_ \/ _].
+
+    As we want to inspect the conclusion of the goal but not the hypotheses,
+    our pattern is of the form [ |- g]. To match for [_ /\ _] and [_ \/ _],
+    we then get the patterns [ [ |- ?a /\ ?b ] ] and  [ |- ?a \/ ?b ].
+*)
+
+Ltac2 and_or_or () :=
+  lazy_match! goal with
+  | [ |- ?a /\ ?b ] => printf "Goal is %t /\ %t" a b
+  | [ |- ?a \/ ?b ] => printf "Goal is %t \/ %t" a b
+  | [ |- _] => Control.zero (Tactic_failure (Some (fprintf
+                "The goal is not a conjunction nor a disjunction")))
+  end.
+
+Goal True /\ False.
+  and_or_or ().
+Abort.
+
+Goal False \/ True.
+  and_or_or ().
+Abort.
+
+Goal nat.
+  Fail and_or_or ().
+Abort.
+
+(** To match for an hypothesis of type [nat] but not to check anything on the goal,
+    we would use the pattern [n : nat |- _] as below. To match for a pair of
+    hypotheses [nat], we would then use the pattern [n : nat, m : nat |- _].
+*)
+
+Goal forall (n : nat) (b : bool) (m : nat), True.
+  intros n b m.
+  lazy_match! goal with
+  | [n : nat |- _] => printf "succeeded, hypothesis %I" n
+  end.
+Abort.
+
+Goal nat -> bool -> nat -> True.
+  intros n b m.
+  lazy_match! goal with
+  | [n1 : nat, n2 : nat |- _] => printf "succeeded, hypothesis %I %I" n1 n2
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** We can see, we do need at least an hypothesis per pattern. If we remove
+    [m : nat] this will now fail.
+*)
+Goal forall (n : nat) (b : bool), True.
+  intros n b.
+  Fail lazy_match! goal with
+  | [n1 : nat, n2 : nat |- _] => printf "succeeded, hypothesis %I %I" n1 n2
+  end.
+Abort.
+
+(** By default the hypotheses are matched from the last one to the first one.
+    This can be seen in the example above as it prints [m], the last variable
+    of type [nat] that was introduced.
+    We can start from the first one, by matching [reverse goal] rather than [goal].
+    For instance, in the example below, [m] is found if we match the goal for
+    [ [h : nat |- _] ] as it is the last hypothesis of type [nat] that was
+    introduced. However, it is [n] that is found if match [reverse goal] as it
+    is the first hypothesis of type [nat] that was introduced.
+*)
+
+Goal forall (n : nat) (b : bool) (m : nat), True.
+  intros n b m.
+  lazy_match! reverse goal with
+  | [n : nat |- _] => printf "succeeded, hypothesis %I" n
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** There must be exactly one goal under focus for it to be possible to match
+    the goal, as otherwise the notion of "the goal" would not have much meaning.
+    If more than one goal is focus, it will hence fail with the error [Not_focussed].
+*)
+
+Goal False /\ True.
+  split.
+  Fail
+  (* all focuses on two goals [False] and [True] *)
+  all: lazy_match! goal with
+  | [ |- _] => ()
+  end.
+Abort.
+
+(** Consequently if you want to match the goals, be sure to focus a single goal first,
+    for instance with [Control.enter : (unit -> unit) -> unit] that applies a
+    tactic [tac : unit -> unit] independently to each goal under focus.
+*)
+
+(* 2.2 Non-Linear Matching *)
+
+(** As for matching terms, matching goals is by default syntactic.
+    However, matching for non-linear variables is a bit more involved.
+    In the non-linear case, variable are matched up to conversions when they appear
+    in different clause, and up to syntax when they appear in the same clause.
+
+    To understand this better, let us look at an example.
+    We could write a version of [eassumption] by matching for the pattern [_ : ?t |- ?t].
+    In this case, as [?t] appears in different clauses, one of hypotheses and
+    in then conclusion, it will hence be matched up to conversion.
+    We can check it works by supposing [0 + 1 = 0] and trying to prove [1 = 0],
+    as [0 + 1] is equal to [1] up to conversion but not syntactically.
+*)
+
+Goal 0 + 1 = 0 -> 1 = 0.
+  intros.
+  lazy_match! goal with
+  | [ _ : ?t |- ?t] => printf "succeeded: %t" t
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** However, if a variable appears several times in a same clause, then it is
+    compared syntactically. For instance, in [ |- ?t = ?t], [?t] is compared
+    syntactically as the it appears twice in the goal which forms one clause.
+*)
+
+Goal 1 + 1 = 2.
+  Fail lazy_match! goal with
+  | [ |- ?t = ?t] => printf "equality is %t" t
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** A subtlety to understand is that only the hole associated to a variable will
+    be compared up to conversion, other symbols are matched syntactically as usual.
+    For instance, if we match for [?t, ~(?t)], the symbol [~] will matched,
+    if one if found then inside the clause ~(X) that it will be compared
+    up to conversion with [?t].
+
+    Consequently, if we have [P], it will fail to match for [P -> False] as
+    [~] is matched syntactically, but [P -> False] is the unfolding of [~P].
+*)
+
+Goal forall P, P -> (P -> False) -> False.
+  intros.
+  Fail match! goal with
+  | [_ : ?t, _ : ~(?t) |- _ ] => printf "succeed: %t" t
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** However, matching for [~((fun _ => P) 0)] will work as [~] will be matched,
+    then [(fun _ => P)0] matched with [P] up to conversion which works.
+*)
+
+Goal forall P, P -> ~((fun _ => P) 0) -> False.
+  intros.
+  match! goal with
+  | [_ : ?t, _ : ~(?t) |- _ ] => printf "succeed: %t" t
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** It often happens that non-linear matching is not precise enough for our
+    purpose, either because we would like to match both term in one clause
+    up to conversion, or because we would like to use a different notation of
+    equality of non-linear occurencess like syntactic equality, equality up to
+    some reduction, or even up to unification.
+
+    In this case, the best approach is to use different variables for each
+    occurences we want to compared, then call the comparaison we wish.
+    For instance, to match for [P] and [~P] up to unification, we would:
+    match for a pair of variables [t1], [t2] then call a unification function
+    to check if one of the hypotheses is indeed a negation of the other.
+*)
+
+Goal forall P, P -> (P -> False) -> False.
+  intros.
+  match! goal with
+  | [ _ : ?t1, _ : ?t2 |- _] =>
+      Unification.unify_with_full_ts t2 '($t1 -> False);
+      printf "success"
+  | [ |- _ ] => fail
+  end.
+Abort.
+
+(** The advantage of this method is that it provides the user with a fine grained
+    control to the user when and how reduction and equality tests are performed.
+*)
+
+(* 3. Backtracking and [lazy_match!], [match!], [multi_match!] *)
+
+(** 3.1 [lazy_match!]
+
+    [lazy_match!] is the easiest command to understand and to use.
+    [lazy_match!] picks a branch, and sticks to it to even if the code excuted
+    after picking this branch (the body of the branch) leads to a failure.
+    It will not backtrack to pick another branch if a choice leads to a failure.
+
+    For instance, in the example below, it picks the first branch as everything
+    matches [[ |- _]]. It prints "branch 1", then fails. As no backtracking is
+    allowed, it stick to this choice and fails.
+*)
+
+Goal False.
+  Fail lazy_match! goal with
+  | [ |- _ ] => printf "branch 1"; fail
+  | [ |- _ ] => printf "branch 2"
+  | [ |- _ ] => printf "branch 3"
+  end.
+Abort.
+
+(** [lazy_match!] should be considered as the default, as it is easy to understand
+    (no backtracking) which prevents unexpected behaviour, and yet sufficient
+    for all applications where matching the syntax is a sufficient to decide what to do.
+
+    A common use of [lazy_match!] is to make a decision based on the shape of the
+    goal or the shape of a term or type.
+
+    As a simple example, let us write a tactic [split_and] that introduces
+    variables and hypotheses with [intros ?] if the goal is of the form [A -> B],
+    splits the goal with [split] if it is a conjunction [A /\ B], and recursively
+    simplify the new goals.
+    In both case, the syntactic equality test is sufficient to decide what to do
+    as if it is of the required form, then the branch will succeed.
+    One should hence use [lazy_match!], which leads to the following simple function:
+*)
+
+Ltac2 rec split_and () :=
+  lazy_match! goal with
+  | [ |- _ -> _ ] => intros ?; split_and ()
+  | [ |- _ /\ _ ] => split > [split_and () | split_and ()]
+  | [ |- _ ] => ()
+  end.
+
+Goal (True /\ ((False /\ True) /\ False)) /\ True.
+  split_and ().
+Abort.
+
+Goal forall (n : nat), (forall m, m = n) /\ (False \/ False) /\ True.
+  split_and ().
+Abort.
+
+Goal True \/ False.
+  Fail (progress (split_and ())).
+Abort.
+(** 3.2 [match!]
+
+      [match! goal with] picks the first branch that matches.
+      Then, if evaluation of its body fails, it backtracks
+      and picks the next matching pattern,
+      potentially the same one if all the hypotheses have not been exhausted yet.
+
+      In the example below the first branch is picked and fails, it hence
+      backtracks to its choice.
+      There is only one possibility for the pattern [ |- _] as it matches any goal.
+      As it has already been tried, it hence switches to the second pattern which is [ |- _].
+      This branch now succeeds, hence the whole [match!].
+*)
+
+Goal False.
+  match! goal with
+  | [ |- _ ] => printf "branch 1"; fail
+  | [ |- _ ] => printf "branch 2"
+  | [ |- _ ] => printf "branch 3"
+  end.
+Abort.
+(** match!] is useful as soon as matching the syntax is not enough, and we
+    need additional tests to see if we have picked the good branch or not.
+    Indeed, if such a test fails raising an exception (or we make it so), then
+    [match!] will backtrack, and look for the next branch matching the pattern.
+
+    A common application of [match!] is to match the goal for hypotheses, then
+    do extra-test to decide what to do, or ensure we have picked the good ones.
+    If we have not, failing or triggering failure, then enables to backtrack and
+    to try the next possible hypotheses.
+
+    A basic example is to recode a simple [eassumption] tactic, that tries
+    to solve the goal with [exact P] for all hypotheses [P].
+    If we match the goal with the pattern [p : _ |- _] to get a [P], it is most
+    likely the first hypothesis [P] picked will not solve the goal, and hence
+    that [exact P] will fail.
+    In this case, we want to backtrack to try the next hypothesis [P].
+
+    It is only if [exact P] succeeds that we know we have picked the good branch.
+    Consequently, we want to use [match!] and not [lazy_match!].
+*)
+
+Ltac2 my_eassumption () :=
+  match! goal with
+  | [p : _ |- _] =>
+      printf "Try %I" p;
+      let p := Control.hyp p in exact $p
+  | [ |- _] => Control.zero (Tactic_failure (Some (fprintf "No such assumption")))
+  end.
+
+Goal forall P Q, P -> Q -> P.
+  intros P Q p q. my_eassumption ().
+Qed.
+
+Goal forall P Q, P -> P -> Q.
+  intros P Q p1 p2. Fail my_eassumption ().
+Abort.
+(** 3.3 [multi_match!]
+
+      [multi_match! goal with] is more complex and subtle. It basically behaves
+      like [match!] except that it will further backtrack if the choice of a
+      branch leads to a subsequent failure when linked with another tactic.
+
+      For instance, in the example below we link the [match!] with [fail], to make
+      the composition fail. In the [match!] case, it will try the first branch,
+      then the second that succeeds, then try [fail], and hence fail.
+      It will hence print [branch 1] and [branch 2], and then fail.
+*)
+
+Goal False.
+  Fail match! goal with
+  | [ |- _ ] => printf "branch 1"; fail
+  | [ |- _ ] => printf "branch 2"
+  | [ |- _ ] => printf "branch 3"
+  end; fail.
+Abort.
+
+(** In contrast, when the composition fails [multi_match!] will further bracktrack
+    to its choice of branch, in this case the second one, and try the next matching branch.
+    The idea is that picking a different branch could have led to the subsequent
+    tactic to succeed, as it can happen when using [constructor].
+    Here, as [fail] always fails, it will still failed but we can see it did
+    backtrack and tried the third branch as it will print [branch 3].
+*)
+
+Goal False.
+  Fail multi_match! goal with
+  | [ |- _ ] => printf "branch 1"; fail
+  | [ |- _ ] => printf "branch 2"
+  | [ |- _ ] => printf "branch 3"
+  end; fail.
+Abort.
+
+(** [multi_match!] is meant to write tactics performing a choice, and that
+    we want to link with other tactics, like the [constructor] tactic
+    that we can then link with [reflexivity] or [assumption] to solve the goal.
+
+    A basic example is to code a tactic that recursively picks [left] or [right]
+    if the goal is for the form [A \/ B], which is similar to [repeat constructor].
+    The choices [left] or [right] are both correct as soon as the goal is of the
+    form [A \/ B]. We can only know if we have picked the good one, once chained
+    with another tactic that tries to solve the goal.
+    We hence need to use [multi_match!] as if we have picked the wrong side
+    to prove, we want to backtrack to pick the otherwiside.
+
+    This leads to the following small script, improved with printing to display
+    the backtracking structure:
+
+*)
+
+Ltac2 rec left_or_right () :=
+  multi_match! goal with
+  | [ |- _ \/ _ ] => print_goals; printf "use left"; left; left_or_right ()
+  | [ |- _ \/ _ ] => print_goals; printf "use right"; right; left_or_right ()
+  | [ |- ?t ] => printf "the final goal is %t" t ; printf "-------"
+  end.
+
+Goal False \/ (False \/ True) \/ 0 = 1.
+  left_or_right (); exact I.
+Abort.
+
+Goal False \/ (False \/ False) \/ (0 = 1 -> 0 = 1).
+  left_or_right (); intros X; exact X.
+Abort.
+
+(** [multi_match!] is **not meant** to be used by default.
+    Yes, it is the more powerful match primitive in terms of backtracking, but it
+    can be hard to understand, predict and debug, in particular for newcomers.
+    Moreover, it can be expensive as it can perform an exponential number of
+    backtracking attempts when linked with another tactic that can backtrack.
+    It should hence only be used when needed.
+*)