# The Tactic Descente Infinie

## Description of di

 "di" is a tactic that helps to prove inductive lemmas by fixpoint functions. People familiar with the "fix" tactic knows that it presupposes the truth of the goal, putting an inductive hypothesis that is of the same type as the goal in the context, by refining a fixpoint function whose type is the goal. However, the tactic "fix" is not consistent, since the hypothesis introduced, which is a fixpoint function, can be applied in a way that breaks its well-foundedness. "di" addresses this problem by applying the fixpoint function on strict subterms of the original arguments and clearing the fixpoint function from the context, so that the user has no chance of breaking the well-foundedness. It has two formats. The simpler one is "di some_id d". This creates a fixpoint function with the decreasing argument as "some_id", where "some_id" must be inductive, and present in the context. It then performs case analysis on "some_id" multiple times, specified by the depth parameter "d". The tactic then finds strict subterms of "some_id" and apply the fixpoint function on them, before clearing it from the context.

For example, if we were to prove the following lemma:

```Inductive even : nat -> Prop :=
| e0 : even 0
| eS : forall n, even n->even (S (S n)).

Goal forall n, even n \/ ~even n.
```
After applying "intro n", we get the following:
```  n : nat
============================
even n \/ ~ even n
```
Now we could apply "di n 2" on it and get 3 subgoals:
```Subgoal 1

============================
even 0 \/ ~ even 0

Subgoal 2
============================
even 1 \/ ~ even 1

Subgoal 3
x0 : nat
IH : even x0 \/ ~ even x0
============================
even (S (S x0)) \/ ~ even (S (S x0))
```
 The three subgoals are obtained by performing case analysis on "n" twice. The first and second subgoal do not contain any subterms of "n" in the original goal, and therefore the inductive hypothesis is simply cleared from the context. In the third subgoal, "x0" is a subterm of "n" in the original goal. Its relationship with "n" is that "n = S (S x0)". The tactic applies the inductive hypothesis "forall n, even n \/ ~even n" on "x0" and obtains the hypothesis "IH", putting it in the context. The same can be achieved by using the second form of "di", which gives the user more flexibility. The format is "di some_id as some_pattern1 hyps some_pattern2". This destructs the hypothesis with the id "some_id" according to the pattern supplied by "some_pattern1". The inductive hypothesis is removed in all subgoals, after applying it according to "some_pattern2". The grammar for the patterns is the same for the one used in coq's tactics like intros, destruct and so on. For the example goal above, we could apply "di n as [| [| x0]] hyps [| [| IH]]" to achieve the same effect. The two patterns must match exactly in shape. The second pattern tells the tactic on which variables it should apply the inductive hypothesis. For the example above, the second pattern tells the tactic to apply the inductive hypothesis on "x0" and name the result "IH", as "x0" and "IH" match in position. There are cases where we do not want to apply the inductive hypothesis on all the variables introduced in the first pattern. For example, for the following goal: ``` n : nat m : nat H : n <= m ============================ S n <= S m ``` If we would like "H" to be the decreasing argument, we can apply "di H as [| m H] hyps [| ? IH]". Since "m" is not a subterm of "H". We do not want to apply the inductive hypothesis on "m". We indicate that to the tactic by putting a question mark "?" in the corresponding position in the second pattern. The result of the application of this tactic is the following two subgoals: ```Subgoal 1: n : nat ============================ S n <= S n Subgoal 2: n : nat m : nat H : n <= m IH : S n <= S m ============================ S n <= S (S m) ```

## Usage

The di tactic can be loaded by

Coq < Declare ML Module "di".

### Format 1

di some_id depth

Example:
```  n : nat
============================
even n \/ ~ even n
```

Coq < di n 2.

```Subgoal 1

============================
even 0 \/ ~ even 0

Subgoal 2
============================
even 1 \/ ~ even 1

Subgoal 3
x0 : nat
IH : even x0 \/ ~ even x0
============================
even (S (S x0)) \/ ~ even (S (S x0))
```

### Format 2

di some_id as some_pattern1 hyps some_pattern2

The two patterns must match exactly in shape. The first pattern tells the tactic how to
destruct the variable with the given identifier. The second pattern tells the tactic on
which variables it should apply the inductive hypothesis. If we do not want to apply
the inductive hypothesis on a certain variable, just put a question mark "?" at its
corresponding position in the second pattern.

Example:

```  n : nat
m : nat
H : n <= m
============================
S n <= S m
```

Coq < di H as [| m H] hyps [| ? IH].

```Subgoal 1:

n : nat
============================
S n <= S n

Subgoal 2:

n : nat
m : nat
H : n <= m
IH : S n <= S m
============================
S n <= S (S m)
```