Stream: Coq users

Topic: Trying to understand behavior of destruct


view this post on Zulip 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.
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.

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (May 05 2022 at 22:23):

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

view this post on Zulip Patrick Nicodemus (May 05 2022 at 22:24):

The first constructor of is listis 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.

view this post on Zulip 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}

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (May 05 2022 at 22:37):

hmm ok.

view this post on Zulip Notification Bot (May 07 2022 at 04:27):

Patrick Nicodemus has marked this topic as unresolved.

view this post on Zulip Notification Bot (May 07 2022 at 04:47):

Patrick Nicodemus has marked this topic as resolved.

view this post on Zulip Notification Bot (May 07 2022 at 05:00):

Patrick Nicodemus has marked this topic as unresolved.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (May 07 2022 at 05:38):

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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (May 07 2022 at 06:05):

inversion p should be helpful here?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Patrick Nicodemus (May 07 2022 at 08:55):

Ok. I will think about this.

view this post on Zulip 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

view this post on Zulip 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' =>  (eq_refl (t0 n))
                       | r1 _ a => inr (f a)
                       end.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 07 2022 at 09:12):

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

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (May 07 2022 at 11:01):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Gaëtan Gilbert (May 07 2022 at 11:40):

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

view this post on Zulip Patrick Nicodemus (May 07 2022 at 22:11):

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

view this post on Zulip Patrick Nicodemus (May 07 2022 at 22:11):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)).

view this post on Zulip Patrick Nicodemus (May 07 2022 at 22:20):

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

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (May 07 2022 at 22:23):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (May 08 2022 at 08:54):

is comp a constructor?

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (May 08 2022 at 10:00):

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

view this post on Zulip 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

view this post on Zulip Patrick Nicodemus (May 08 2022 at 10:14):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Ali Caglayan (May 08 2022 at 16:57):

Oh nevermind, I got confused with discriminate

view this post on Zulip Patrick Nicodemus (May 09 2022 at 12:34):

Discriminate has worked for me!


Last updated: Jan 31 2023 at 12:01 UTC