## Stream: Coq users

### Topic: Unique indices in list

#### Adrián García (Mar 15 2022 at 02:35):

I'm trying to define a context of hypotheses with a snoc list, where the hypotheses are pairs of numbers and formulas, like so:

``````Inductive slist (X: Type): Type :=
| empty : slist X
| snoc : slist X -> X -> slist
Definition LabelledHyp : Type := (nat * Formula)%type.
Definition LCtx : Type := slist LabelledHyp.
``````

Is it possible to define a snoc list where the mere definition states that the hypotheses indices are in ascendant order and are unique in the whole context? An example would look like:

``````Check (empty, (pair 0 (Varp 0)), (pair 1 (Varp 1)), (pair 2 (Varp 2)))
``````

#### Pierre Castéran (Mar 15 2022 at 06:31):

You may define a Boolean function `test_indices X : slist X -> bool` which checks whether the indices are OK. If you want to define a type for correct slists, you can consider something like `Definition my_context X := {s : slist X | is_true (test_indices _ s)}` or a `Record` definition.

#### Ali Caglayan (Mar 15 2022 at 12:40):

You can also encode it directly into the type of the list, however I don't know how to do this without fixing a length for the list. Therefore you have to sum them up to collect all the lists.

``````Axiom Formula : Type.
Inductive slist (X : Type) : nat -> Type :=
| empty : slist X 0
| snoc {n} : slist X n -> X -> slist X (S n).
Definition LCtx : Type := {n : nat & slist Formula n}.
``````

#### Ali Caglayan (Mar 15 2022 at 12:42):

That also might be a bit harder to work with than Pierre's suggestion since reasoning about indexed inductive types can be tricky. The advantage of this approach is that you can't write down a malformed list.

#### Meven Lennon-Bertrand (Mar 15 2022 at 13:32):

If I understand the demand correctly, you want something like

``````Inductive slist : nat -> Type :=
| empty : slist 0
| snoc (f : Formula) (m n : nat) : slist n -> n < m -> slist m.

Definition LCtx : Type := {n : nat & slist n}.
``````

rather than @Ali Caglayan's definition, no? (The point being that the indices need not be the integers one after another, @Ali Caglayan's `slist` is exactly `Vector.t`, and his `LCtx` is isomorphic to `list Formula`).
If you want the indices to be those, then I don’t think storing them in the list is wise, and using a regular `list Formula` should be enough (you can always reconstruct the index by talking about the position).

#### Ali Caglayan (Mar 15 2022 at 13:34):

Right that makes more sense.

#### Pierre Castéran (Mar 15 2022 at 16:10):

Yes, but it depends on whether you assume the sequence of indices is always of the form (0,1,2,...,n) or if it is any strictly increasing sequence of `nat`s (with possible holes).

#### Adrián García (Apr 02 2022 at 23:23):

Thank you to all of you for your help, I was testing some of those solutions but then I found this where they define the `pred_safe` program (page 7) or the bounded arrays (page 11).

It seems to be closer to what I would like to achieve, to create snoc lists where the indices are unique no matter the order. So I defined a function to check if the index is an unique one:

``````Inductive slist (X: Type): Type :=
| empty : slist X
| snoc : slist X -> X -> slist
Definition LabelledHyp : Type := (nat * Formula)%type.

Fixpoint not_used_index (h: LabelledHyp) (G: slist LabelledHyp) : Prop :=
match G with
| empty => True
| G', h' => (fst h) <> (fst h') /\ not_used_index h G'
end.
``````

and the inductive definition itself:

``````Inductive lctx : Type :=
| emptyc : lctx
| snocc : forall (h : LabelledHyp) (G : slist LabelledHyp),
not_used_index h G -> lctx.
``````

but how can I construct an example of that lctx? Or my definitions are not useful to create instances like `emptyc, (pair 0 (Varp 0))` ?

#### Pierre Castéran (Apr 03 2022 at 06:46):

Hi!

Your definition of `lctx` doesn't prevent you from building lists with repeated indices.
Here's is an example:

``````Module OriginalDef.
Inductive lctx : Type :=
| emptyc : lctx
| snocc : forall (h : LabelledHyp) (G : slist LabelledHyp),
not_used_index h G -> lctx.

Let g := snoc (snoc empty (2, Varp 42)) (2, Varp 50).

Definition g': lctx.
refine (snocc (1, Varp 89) g _).
simpl; repeat split; auto.
Defined.

End OriginalDef.
``````

A possible solution is to work with `sig`types.

``````(* TODO:  replace Prop with bool *)
Fixpoint nodup_index (G: slist  LabelledHyp) : Prop :=
match G with
| empty  => True
| snoc G' h' => not_used_index h' G' /\ nodup_index G'
end.

(* lists with distinct keys *)
Definition lctx := {l : slist LabelledHyp | nodup_index l}.

Definition mylist : lctx.
Proof.
exists  (snoc   empty (0, Varp 42)).
simpl;tauto.
Defined.

Definition mylist2 : lctx.
Proof.
exists  (snoc (snoc  empty (0, Varp 42)) (1, Varp 33)).
simpl. repeat split; discriminate.
Defined.
``````

Please note that you can simulate your `snocc`constructor (with a slightly different type).

``````Definition data (G: lctx):= proj1_sig G.

Definition snocc (h: LabelledHyp)(G:lctx) (H: not_used_index h (data G)): lctx.
Proof.
exists  (snoc (data G) h );split ; [destruct G; tauto |trivial].
Defined.

Definition mylist2' : lctx.
Proof.
refine (snocc (2,Varp 50) mylist2 _).
simpl; intuition discriminate.
Defined.

(* rejected definition (duplication of  index 1 ) *)
Definition mylist3 : lctx.
refine (snocc (1,Varp 50) mylist2 _); cbn.
Abort.
``````

By the way, I'm not familiar with `snoc` lists. What's the advantage over "normal" stdlib's lists ?
Pierre

#### Adrián García (May 02 2022 at 04:09):

Thanks for your help Pierre! I ended up using your definition of lctx as:

``````Definition lctx := {l : slist LabelledHyp | nodup_index l}.
``````

now I'm facing a problem about how to actually use it on this inductive definition:

``````Inductive dummy : lctx -> lctx -> Formula -> Prop :=

| dummy_hyp : forall (D: lctx) (G G': lctx) (A: Formula),
let L := (proj1_sig G), (0 -: A) : lctx in
DC_Proof D (concat L G') A.
``````

so I'm trying to construct a `lctx L` by adding a new hypothesis A to the right, but obviously I get an error, so how do I actually construct the sig type? Using `exist`?

And answering your question about why using snoc lists, the only "advantage" is that they are more "human readable" than normal lists, at least for what I'm trying to achieve

#### Pierre Castéran (May 02 2022 at 06:31):

Do you want to add a labelled hypothesis at the right of a `lctx`?
If so, here is a possible solution:

``````Require Import Program.Tactics.

(l:lctx)(h: LabelledHyp)(H: not_used_index h l): lctx :=
exist _ (snoc l  h) _.
Next Obligation.
split; [| assumption]; now destruct l.
Defined.
``````

A few remarks:

• You may also define `not_used_index` and `nodup_index`as boolean functions instead of predicates, in Ssr style, since `key`is a type with decidable equality.

• If you extend `addr` to a function which appends two `lctx`, you will have to prove first a few lemmas about lists without duplicates.

• Last, about `snoc`. If a library about such lists is missing, you will probably have to define functions and prove properties which already exist about "classic" lists. In developments where readability matters, you may also define helper functions just for I/O, and use libraries for the rest.

#### Adrián García (May 16 2022 at 04:02):

Hi Pierre !

As you said, I'm figuring out how to prove some lemmas about lists without dups and also some functions/properties about snoc. Also I'm trying to replace my simple lists for this new `lctx` sigma type but I found myself in this situation:

``````Definition lctx := { l: slist LabelledHyp | no_dup l }.
Theorem foo:
forall (G D : lctx) (A: Formula),
DC_Proof G D A.
intro G.
destruct G as [L H].
induction L.
- intros.
``````

I need to use induction on lctx, but how can I replace the exist term that appears on the goal?

``````1 goal
H : no_dup empty
D : lctx
A : Formula
______________________________________(1/1)
exist (fun l : slist LabelledHyp => no_dup l) empty H ∥ D ⊢s A
``````

can I replace it or simplify it so I could be able to continue with the induction?

#### Pierre Castéran (May 16 2022 at 07:18):

Do you mean you want to define a concatenation of two `lctx` (under some condition) ?
A possible way is to prove first a lemma like "Let `l`and `l'` be two snoc lists without duplicate index, and such that the indexes of `l` and `l'`are disjoint, then the concatenation of `l`and `l'` has no duplicate". Then you prove your result on `lctx`.
It may be possible to define directly your concatenation with `Program Fixpoint` too.

I could not find the definition of `DC_Proof` nor the notation used in your goal. The best would be to give access to a replayable snippet.

Pierre

#### Adrián García (May 22 2022 at 19:53):

Hello Pierre,

I defined the concatenation of two `lctx` like this:

``````Definition concat (G G': lctx): lctx.
Proof.
destruct G  as [L  H].
destruct G' as [L' H1].
exists (rec_concat L L').
apply no_dup_concat.
exact H.
exact H1.
Qed.
``````

where `rec_concat` its a fixpoint that creates a new `lctx` and `no_dup_concat` its a lemma, but that's not my actual problem.

The thing is that whenever I try to proof something by induction on an `lctx`, first I destruct the sigma type and then I try induction on the resulting `slist LabelledHyp`, but I cannot get rid of the `exist (fun l : slist LabelledHyp => no_dup l) empty H`, I would like to just keep the `empty` lctx and `(L, x)` lctx on the inductive step

``````Theorem foo:
forall (G: lctx),
G = G.
intro G.
destruct G as [L H].
induction L.
- intros.
``````

(really dummy example but just to illustrate my question)

``````1 goal
H : no_dup empty
______________________________________(1/1)
exist (fun l : slist LabelledHyp => no_dup l) empty H =
exist (fun l : slist LabelledHyp => no_dup l) empty H
``````

#### Paolo Giarrusso (May 22 2022 at 20:26):

`f_equal` handles this, but it's a good question

#### Paolo Giarrusso (May 22 2022 at 20:47):

I'd say you want sigma types to come with lemmas like `slist_eq_intro` — which depend on proof irrelevance.

``````Lemma slist_eq_intro l1 l2 H1 H2 :
l1 = l2 ->
mk_lctx l1 H1 = mk_lctx l2 H2.
Proof.
intros ->. f_equal.
(* Goal: H1 = H2. How to proceed? *)
``````

You can use a proof irrelevance axiom, but that's overkill; you can just make `no_dup` produce a boolean, use `no_dup l = true`, and exploit proof irrelevance of boolean equality. You'd usually end up wanting to define both a `bool` and `Prop` version of `no_dup` and relate them — but thankfully, typeclasses let you define just the `Prop` version and derive a good boolean one semi-automatically. Here's a possible solution:

``````From stdpp Require Import prelude.

Inductive slist {X : Type} : Type :=
| empty : slist
| snoc : slist -> X -> slist.
Arguments slist : clear implicits.
Axiom Formula : Type.
Definition LabelledHyp : Type := nat * Formula.
Fixpoint not_used_index (h: LabelledHyp) (G: slist LabelledHyp) : Prop :=
match G with
| empty => True
| snoc G' h' => fst h <> fst h' /\ not_used_index h G'
end.
#[export] Instance not_used_index_dec h G : Decision (not_used_index h G).
Proof. induction G; apply _. Defined.

Fixpoint nodup (G: slist LabelledHyp) : Prop :=
match G with
| empty  => True
| snoc G' h' => not_used_index h' G' /\ nodup G'
end.
#[export] Instance nodup_dec G : Decision (nodup G).
Proof. induction G; apply _. Defined.

Definition lctx := { l: slist LabelledHyp | bool_decide (nodup l) }.
Definition mk_lctx (l : slist LabelledHyp) (H : nodup l ) : lctx :=
exist _ l (bool_decide_pack _ H).

Lemma slist_eq_intro l1 l2 H1 H2 :
l1 = l2 ->
mk_lctx l1 H1 = mk_lctx l2 H2.
Proof.
intros ->. unfold mk_lctx; f_equal.
apply proof_irrel.
Qed.
Print Assumptions slist_eq_intro.
(*
Axioms:
Formula : Type
*)
``````

#### Paolo Giarrusso (May 22 2022 at 20:50):

If you want, one can avoid stdpp and use the stdlib only (and I'm sure mathcomp also gives good solutions, but I'm not good with that).

#### Paolo Giarrusso (May 22 2022 at 20:51):

especially if you're happy with a proof-irrelevance axiom.

#### Paolo Giarrusso (May 22 2022 at 20:53):

but I don't know how to restrict to the stdlib without getting something that (personally) I'd consider worse (less maintainable/more duplication/...)

Last updated: Jun 23 2024 at 03:02 UTC