## Stream: Coq users

### Topic: Trying to understand behavior of destruct

#### Patrick Nicodemus (May 05 2022 at 22:22):

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.

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.
``````

#### Patrick Nicodemus (May 05 2022 at 22:23):

So in this script, `lct_is_list` is of type ` lct_is_list : is_list n m lct_new`

#### Patrick Nicodemus (May 05 2022 at 22:23):

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

#### Patrick Nicodemus (May 05 2022 at 22:24):

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.

#### Patrick Nicodemus (May 05 2022 at 22:25):

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}
``````

#### Patrick Nicodemus (May 05 2022 at 22:25):

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.

#### Patrick Nicodemus (May 05 2022 at 22:26):

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

#### Patrick Nicodemus (May 05 2022 at 22:27):

``````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

#### Patrick Nicodemus (May 05 2022 at 22:27):

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

(after)

#### Patrick Nicodemus (May 05 2022 at 22:27):

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

#### Patrick Nicodemus (May 05 2022 at 22:27):

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

#### Gaëtan Gilbert (May 05 2022 at 22:35):

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 (May 06 2022 at 00:18):

Yo, that worked! Thank you!

#### Notification Bot (May 06 2022 at 00:18):

Patrick Nicodemus has marked this topic as resolved.

#### Notification Bot (May 07 2022 at 04:27):

Patrick Nicodemus has marked this topic as unresolved.

#### Notification Bot (May 07 2022 at 04:47):

Patrick Nicodemus has marked this topic as resolved.

#### Notification Bot (May 07 2022 at 05:00):

Patrick Nicodemus has marked this topic as unresolved.

#### Patrick Nicodemus (May 07 2022 at 05:03):

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?

#### Patrick Nicodemus (May 07 2022 at 05:36):

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.
``````

#### Patrick Nicodemus (May 07 2022 at 05:38):

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

#### Patrick Nicodemus (May 07 2022 at 05:39):

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.

#### Paolo Giarrusso (May 07 2022 at 06:05):

`inversion p` should be helpful here?

#### Patrick Nicodemus (May 07 2022 at 07:39):

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)

#### Patrick Nicodemus (May 07 2022 at 07:40):

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

#### Patrick Nicodemus (May 07 2022 at 07:40):

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

#### Gaëtan Gilbert (May 07 2022 at 08:47):

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)`

#### Patrick Nicodemus (May 07 2022 at 08:55):

I am playing around with `match` trying to see how to use dependent pattern matching to solve this kind of problem

#### Patrick Nicodemus (May 07 2022 at 08:55):

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

#### Patrick Nicodemus (May 07 2022 at 08:56):

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.

#### Gaëtan Gilbert (May 07 2022 at 09:11):

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.
``````

#### Gaëtan Gilbert (May 07 2022 at 09:12):

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

#### Patrick Nicodemus (May 07 2022 at 11:00):

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.

#### Patrick Nicodemus (May 07 2022 at 11:01):

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

#### Patrick Nicodemus (May 07 2022 at 11:02):

``````  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
``````

#### Patrick Nicodemus (May 07 2022 at 11:03):

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.

#### Patrick Nicodemus (May 07 2022 at 11:08):

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.

#### Patrick Nicodemus (May 07 2022 at 11:09):

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)).
``````

#### Gaëtan Gilbert (May 07 2022 at 11:16):

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.
``````

#### Gaëtan Gilbert (May 07 2022 at 11:31):

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

#### Gaëtan Gilbert (May 07 2022 at 11:32):

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.
``````

#### Gaëtan Gilbert (May 07 2022 at 11:37):

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

#### Gaëtan Gilbert (May 07 2022 at 11:40):

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

#### Patrick Nicodemus (May 07 2022 at 22:11):

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

#### Patrick Nicodemus (May 07 2022 at 22:11):

I will explain my design strategy.
Can you tell me if my design strategy makes sense?

#### Patrick Nicodemus (May 07 2022 at 22:14):

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.

#### Patrick Nicodemus (May 07 2022 at 22:15):

``````  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

#### Patrick Nicodemus (May 07 2022 at 22:16):

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.

#### Patrick Nicodemus (May 07 2022 at 22:18):

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.

#### Patrick Nicodemus (May 07 2022 at 22:18):

``````  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)).
``````

#### Patrick Nicodemus (May 07 2022 at 22:20):

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

#### Patrick Nicodemus (May 07 2022 at 22:22):

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.

#### Patrick Nicodemus (May 07 2022 at 22:23):

Then after I destruct `l` I get three branches in the proof, i.e.

#### Patrick Nicodemus (May 07 2022 at 22:24):

`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)`

#### Patrick Nicodemus (May 07 2022 at 22:25):

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

#### Patrick Nicodemus (May 07 2022 at 22:26):

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.

#### Gaëtan Gilbert (May 08 2022 at 08:54):

is comp a constructor?

#### Patrick Nicodemus (May 08 2022 at 09:59):

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`

#### Patrick Nicodemus (May 08 2022 at 10:00):

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

#### Gaëtan Gilbert (May 08 2022 at 10:08):

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

#### Patrick Nicodemus (May 08 2022 at 10:14):

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

#### Patrick Nicodemus (May 08 2022 at 10:50):

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.

#### Ali Caglayan (May 08 2022 at 16:55):

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?

#### Ali Caglayan (May 08 2022 at 16:57):

Oh nevermind, I got confused with discriminate

#### Patrick Nicodemus (May 09 2022 at 12:34):

Discriminate has worked for me!

Last updated: Oct 03 2023 at 19:01 UTC