Destruct / induction isn't behaving the way I expect it to in a piece of my code, I'd be grateful if somebody could explain what the error is here.

```
From HoTT Require Import Basics Types Spaces.Nat.
Notation "n < k" := (lt n k).
Notation "n .+1" := (S n).
Proposition mixed_trans1 : forall n m k : nat, n <= m -> m < k -> n < k.
Proof.
Admitted.
Context `{Funext}.
Definition stdfinset (n: nat) := { m : nat | m < n }.
Inductive Arr : nat -> nat -> Type :=
| d {n : nat} : forall i : stdfinset (n.+1), Arr n n.+1
| s {n : nat } : forall i : stdfinset (n.+1), Arr n.+2 n.+1
| comp {n m k} : forall f : Arr n m, forall g : Arr m k, Arr n k
| id : forall n : nat, Arr n n.
Inductive is_list : forall n m : nat, Arr n m -> Type :=
| is_id {n : nat} : is_list n n (id n)
| tail_is_face {n m : nat} {tree : Arr n m} :
forall p : (is_list n m tree), forall i : (stdfinset m.+1),
is_list n m.+1 (comp tree (d i))
| tail_is_degen {n m : nat} {tree : Arr n m.+2} :
forall p : (is_list _ _ tree), forall i : (stdfinset m.+1),
is_list n m.+1 (comp tree (s i)).
Definition simplicial_bubblesort_single_pass
(n m : nat) (tree : Arr n m) (p : is_list n m tree) :
{ newTree : Arr n m & is_list _ _ newTree }.
Proof.
induction p; [ exact (id n; is_id) | |]; clear tree p;
destruct IHp as [lct_new lct_is_list]. {
destruct lct_is_list as [ | ? ? lcct lcct_is_list j | ? ? lcct lcct_is_list j].
+ exists (comp (id n) (d i)); apply tail_is_face, is_id.
+ destruct (@leq_dichot i.1 j.1) as [i_leq_j | i_gt_j].
* assert (i.1 < m.+1) as ibd'. { destruct j as [jval jbd]. simpl in i_leq_j.
unfold "<".
apply leq_S_n'.
apply leq_S_n in jbd.
apply (@leq_trans i.1 jval m i_leq_j jbd). }
assert (j.1.+1 < m.+2) as jbd'. { apply leq_S_n', j.2. }
set (j' := (j.1.+1 ; jbd') : stdfinset m.+2).
exists (comp (comp lcct (d (i.1; ibd'))) (d (j.1.+1; jbd'))).
apply tail_is_face, tail_is_face, lcct_is_list.
* exists (comp (comp lcct (d j)) (d i)); apply tail_is_face, tail_is_face, lcct_is_list.
+ exists (comp (comp lcct (s j)) (d i)). apply tail_is_face, tail_is_degen, lcct_is_list.
}
destruct lct_is_list.
```

So in this script, `lct_is_list`

is of type ` lct_is_list : is_list n m lct_new`

and I was expecting that I could just destruct it to get a case analysis.

The first constructor of `is list`

is of type `is_list n n (id n)`

so my expectation is that when i destruct it, in that case it replaces both of its arguments by one single variable.

So here's my context before I run `destruct lct_as_list`

```
n, m : nat
i : stdfinset m.+1
lct_new : Arr n m
lct_is_list : is_list n m lct_new
============================
{newTree : Arr n m.+1 & is_list n m.+1 newTree}
```

and this is the context after.

```
n : nat
i : stdfinset n.+1
============================
{newTree : Arr n n.+1 & is_list n n.+1 newTree}
```

So I consider this to be the expected behavior.

But in the very last line of the script, I run the command again, and what I get there is

```
n, m : nat
i : stdfinset m.+1
lct_new : Arr n m.+2
lct_is_list : is_list n m.+2 lct_new
============================
{newTree : Arr n m.+1 & is_list n m.+1 newTree}
```

(before

```
m : nat
i : stdfinset m.+1
n : nat
============================
{newTree : Arr n m.+1 & is_list n m.+1 newTree}
```

(after)

What i'd like to know is, why doesn't it replace the two variables with one?

and how can i achieve the desired goal which is to reduce to the case of the first constructor

because you have m.+2

destruct/induction only knows how to handle indices when they are distinct variables

when they are not variables it will first generalize which loses information

you can try `remember m.+2 as m'`

(it should replace the m.+2 in your hypothesis by a new m' and add an hypothesis m' = m.+2) then destruct

hmm ok.

Patrick Nicodemus has marked this topic as unresolved.

Patrick Nicodemus has marked this topic as resolved.

Patrick Nicodemus has marked this topic as unresolved.

Ok, that was really helpful. Is there a way I can adapt this to the case where `m.+2`

can't be abstracted because other things depend on it?

Been thinking about how to illustrate my problem with a good example

```
Inductive Q : nat -> nat -> Type :=
| t0 : forall n, Q n n.+1
| t1 : forall n, Q n n.+1.
Variable A B : Type.
Variable f : A -> B.
Inductive P : forall n m : nat, forall x : Q n m, Type :=
| r0 : forall n : nat, P n n.+1 (t0 n)
| r1 : forall n : nat, forall a : A, P n n.+1 (t1 n).
Proposition test : forall n : nat, P n n.+1 (t1 n) -> B.
Proof.
intros n p.
induction p.
remember n.+1 as m eqn:E.
```

The remember command won't work here because the type of `(t1 n)`

.

My idea is that I know that `r1`

is the only constructor of `P n n.+1 (t1 n)`

in general so I should be able to reduce to that case.

`inversion p`

should be helpful here?

I was using the homotopy type theory library and I don't think they have written the inversion tactic for it yet (i.e. which would use the HoTT equality rather than the vanilla Coq equality)

I would imagine it's just a matter of updating the pointers in the script to point to the right file but idk

Anyway, I guess I'm just punishing myself at this point, the inversion tactic does sound like what i need

Patrick Nicodemus said:

Ok, that was really helpful. Is there a way I can adapt this to the case where

`m.+2`

can't be abstracted because other things depend on it?

in general no, but depending on the specifics you can do some things

in this example

```
Proposition test : forall n : nat, P n (S n) (t1 n) -> B.
Proof.
intros n p.
assert (Ht : Q_rect (fun _ _ _ => Prop) (fun _ => False) (fun _ => True) n (S n) (t1 n)) by exact I.
(* or
assert (Ht : match t1 n return Prop with t0 _ => False | t1 _ => True end) by exact I. *)
generalize dependent (t1 n);intros.
remember (S n) as m eqn:E.
induction p.
- destruct Ht.
- exact (f a).
Qed.
```

the trick is that the `S n`

in the type of `Ht`

can be generalized if we generalize the occurence in the type of `t1'`

at the same time, unlike the type of the equation from remember `t1' = t1 n :> Q n (S n)`

Ok. I will think about this.

I am playing around with `match`

trying to see how to use dependent pattern matching to solve this kind of problem

```
Definition b_from_p := match p in (P n (S n) (t1 n)) return (t0 n = t1 n) + B with
| r0 k as p' => (eq_refl (t0 n))
| r1 _ a => inr (f a)
end.
```

My idea was that if I could return a proof of `t0 = t1`

in this dependent match statement I could use this to derive a contradiction.

equations can also do some stuff, this term is pretty big for what it does though

```
Require Import Equations.Equations.
Inductive Q : nat -> nat -> Type :=
| t0 : forall n, Q n (S n)
| t1 : forall n, Q n (S n).
Variable A B : Type.
Variable f : A -> B.
Inductive P : forall n m : nat, forall x : Q n m, Type :=
| r0 : forall n : nat, P n (S n) (t0 n)
| r1 : forall n : nat, forall a : A, P n (S n) (t1 n).
Derive Signature for P.
Proposition test : forall n : nat, P n (S n) (t1 n) -> B.
Proof.
intros n p.
depelim p.
- rewrite (Eqdep_dec.UIP_refl_nat n H) in H0.
simpl in H0.
discriminate.
- exact (f a).
Qed.
Print test.
```

I don't know equations well so maybe there's a better tactic to use

Gaëtan Gilbert said:

Patrick Nicodemus said:

Ok, that was really helpful. Is there a way I can adapt this to the case where

`m.+2`

can't be abstracted because other things depend on it?in general no, but depending on the specifics you can do some things

in this example`Proposition test : forall n : nat, P n (S n) (t1 n) -> B. Proof. intros n p. assert (Ht : Q_rect (fun _ _ _ => Prop) (fun _ => False) (fun _ => True) n (S n) (t1 n)) by exact I. (* or assert (Ht : match t1 n return Prop with t0 _ => False | t1 _ => True end) by exact I. *) generalize dependent (t1 n);intros. remember (S n) as m eqn:E. induction p. - destruct Ht. - exact (f a). Qed.`

the trick is that the

`S n`

in the type of`Ht`

can be generalized if we generalize the occurence in the type of`t1'`

at the same time, unlike the type of the equation from remember`t1' = t1 n :> Q n (S n)`

Ok, cool. This makes sense, I see what's going on here. This helped me with my problem and got me a couple steps forward but I lost some aspects of the problem when I tried to simplify it down to something manageable, so I'm not out of the woods yet.

I'll come back and take a look at it later.

```
n, m : nat
f : Arr n m
p : is_list n m f
i : stdfinset m.+1
j : stdfinset m.+2
T : Last_Entry_Correct n m.+2 ((f · d i) · d j)
============================
i.1 < j.1
```

My current goal looks like this. Here, an `Arr n m`

satisfying the `is_list`

predicate is a list of composable morphisms from `n`

to `m`

. There are two types of nodes that can occur in the list, either `d`

nodes and `s`

nodes, and each node carries a natural number label.

The `Last_Entry_Correct`

is an inductively defined predicate with three branches, one for the case when the list is empty, one for when it ends in a `d`

node and one for when the list ends in an `s`

node. I want to somehow get from the assumption `T`

to the inputs associated to the constructor for `d`

nodes. In this case abstracting away from `i`

and `j`

leaves me unable to solve the goal because i no longer have any interesting information about `i`

and `j`

in my context.

Here is the inductive constructor.

```
Inductive Last_Entry_Correct : forall n m : nat, forall f : Arr n m, Type :=
| base_case {n : nat} : Last_Entry_Correct n n (id n)
| face_case {n m : nat} : forall list : Arr n m, forall p' : is_list n m list,
forall i : stdfinset m.+1,
forall k : (Greatest_Omission (Arr_eval (comp list (d i))) i),
Last_Entry_Correct n m.+1 (comp list (d i))
| degen_case { n m : nat} : forall list : Arr n m.+2, forall p' : is_list n m.+2 list,
forall i : stdfinset m.+1,
forall surj : surjective (Arr_eval (comp list (s i))),
forall k : Least_hits_twice (Arr_eval (comp list (s i))) i,
Last_Entry_Correct n m.+1 (comp list (s i)).
```

maybe you can define a custom eliminator

```
Definition P_elim
(T0:nat -> Type)
(T1:nat -> Type)
(v0:forall n, T0 n)
(v1:forall n, A -> T1 n)
n m q (x:P n m q)
: match q in Q n m with
| t0 n => T0 n
| t1 n => T1 n
end
:=
match x with
| r0 n => v0 n
| r1 n a => v1 n a
end.
Proposition test : forall n : nat, P n (S n) (t1 n) -> B.
Proof.
intros n.
apply (P_elim (fun _ => True) (fun _ => B)).
- exact (fun _ => I).
- intros _ a;exact (f a).
Qed.
```

or something like

```
Definition P_recognizer n m q (x:P n m q) :
sum { H : m = S n & transport _ H q = t0 n }
{ H : m = S n & (A * (transport _ H q = t1 n))%type } :=
match x with
| r0 n => inl (existT _ eq_refl eq_refl)
| r1 n a => inr (existT _ eq_refl (a, eq_refl))
end.
Proposition test : forall n : nat, P n (S n) (t1 n) -> B.
Proof.
intros n p.
destruct (P_recognizer _ _ _ p) as [[Hn Ht]|[Hn [a Ht]]].
all: rewrite (Eqdep_dec.UIP_refl_nat _ Hn) in Ht;simpl in Ht.
- discriminate.
- exact (f a).
Qed.
```

P_recognizer transforms an inductive into something using just sum/sigma/nondependent sigma/equality

can also be written as

```
Definition P_recognizer n m q (x:P n m q) :
sum (existT _ m q = existT _ (S n) (t0 n))
(A * (existT _ m q = existT _ (S n) (t1 n))) :=
match x with
| r0 n => inl eq_refl
| r1 n a => inr (a, eq_refl)
end.
Proposition test : forall n : nat, P n (S n) (t1 n) -> B.
Proof.
intros n p.
destruct (P_recognizer _ _ _ p) as [H|[a H]].
- discriminate.
- exact (f a).
Qed.
```

in the fully general case it's a sum of `{ all_ctor_args : ctor_arg_types & product_of_original indices = product_of_indices_as_in_the_ctor}`

for each constructor, so eg the first one should be

```
{ n' : nat & (n ; (m ; q)) = (n' ; (S n' ; t0 n') }
```

but we can simplify a bit since the first index of P behaves as a parameter

then you use the usual hott lemmas to manipulate the equality between dependent pairs

Ok. I might try to just rewrite some definitions and approach this problem a different way.

I will explain my design strategy.

Can you tell me if my design strategy makes sense?

I am working with a data type of lists, the nodes in the list are of two types, "d" or "s", and the nodes carry natural numbers attached to them. I defined lists as an inductive data type with three constructors.

```
Inductive is_list : forall n m : nat, Arr n m -> Type :=
| is_id {n : nat} : is_list n n (id n)
| tail_is_face {n m : nat} {tree : Arr n m} :
forall p : (is_list n m tree), forall i : (stdfinset m.+1),
is_list n m.+1 (comp tree (d i))
| tail_is_degen {n m : nat} {tree : Arr n m.+2} :
forall p : (is_list _ _ tree), forall i : (stdfinset m.+1),
is_list n m.+1 (comp tree (s i)).
```

i.e. the empty list, (list, i) -> list :: d i, (list, j) -> list :: s j

I am trying to prove the correctness of my sorting algorithm, it's a kind of bubblesort and so I defined an inductive invariant which intends to say that the last element in the list is in the correct place, i.e. is greatest; the idea is that every pass of the bubblesort loop ends up with the greatest element in the list at the last position in the subloop.

The inductive invariant itself is defined in three cases - one for each of the constructors of is_list, depending on whether the list is empty, ends in a d-node or ends in an s-node.

```
Inductive Last_Entry_Correct : forall n m : nat, forall f : Arr n m, Type :=
| base_case {n : nat} : Last_Entry_Correct n n (id n)
| face_case {n m : nat} : forall list : Arr n m, forall p' : is_list n m list,
forall i : stdfinset m.+1,
forall k : (Greatest_Omission (Arr_eval (comp list (d i))) i),
Last_Entry_Correct n m.+1 (comp list (d i))
| degen_case { n m : nat} : forall list : Arr n m.+2, forall p' : is_list n m.+2 list,
forall i : stdfinset m.+1,
forall surj : surjective (Arr_eval (comp list (s i))),
forall k : Least_hits_twice (Arr_eval (comp list (s i))) i,
Last_Entry_Correct n m.+1 (comp list (s i)).
```

What I am asking is - is this a sensible definition of the inductive invariant?

Like, in my proof I want to assume `Last_Entry_Correct l`

and then induct on the structure of the list `l`

, which can be empty, end in a d-node or an s-node.

Then after I destruct `l`

I get three branches in the proof, i.e.

`a : Last_Entry_Correct n n (id n)`

`a : Last_Entry_Correct n m (list :: d i)`

`a : Last_Entry_Correct n m (list :: s i)`

and somehow in each branch I want to replace that assumption `a`

with the form that I know it must have, given the form of the list which we're talking about, namely in the first case it should be `base_case`

, in the second it should be of type `face_case n m i`

and so on

I am not really experienced with like, "logic programming" and I don't know if this is the correct way to formalize this kind of argument, or whether this is the right definition of the inductive type given what i'm trying to do.

is comp a constructor?

Gaëtan Gilbert said:

is comp a constructor?

Comp is a constructor associated to an inductive data type, yes, it's a list concatenation operator, you can read it as `(comp list (s i)) = list :: s i`

unfortunately I don't think the HoTT library has `injection`

set up either

you should be able to write Last_Entry_Correct as a definition

```
Definition Last_Entry_Correct n m f :=
match f with
| id n => unit
(* I'm guessing at what the implicit arguments of comp are here *)
| @comp n m list (d i) => is_list n m list /\ Greatest_Omission (Arr_eval (comp list (d i))) i
| comp list (s i) => exercise to the reader
end.
```

you can either use the definition everywhere, or keep the inductive and prove it equivalent to the definition

Ok, yeah. It makes sense. I'm having trouble proving anything with the inductive definition.

I think the `Definition`

is probably better. The other way contains redundant information that I have to prove is equal wherever it occurs. Getting rid of the redundant information circumvents the problem.

Patrick Nicodemus said:

unfortunately I don't think the HoTT library has

`injection`

set up either

injection ought to work, have you got an example where it doesn't?

Oh nevermind, I got confused with discriminate

Discriminate has worked for me!

Last updated: Jan 31 2023 at 12:01 UTC