Patrick Nicodemus (May 05 2022 at 22:22): 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.
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 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.
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}
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
Patrick Nicodemus (May 05 2022 at 22:37):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.
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.+2can'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):Ok. I will think about this.
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.
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.
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.+2can't be abstracted because other things depend on it?in general no, but depending on the specifics you can do some things
in this exampleProposition 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 nin the type ofHtcan be generalized if we generalize the occurence in the type oft1'at the same time, unlike the type of the equation from remembert1' = 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
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)).
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
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.
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)).
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
injectionset 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 13 2024 at 01:02 UTC