Adrián García (Mar 15 2022 at 02:35): 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)))
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}.
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 nats (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 sigtypes.
(* 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 snoccconstructor (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):Hi, Adrian !
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.
#[program] Definition addr
(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_indexas boolean functions instead of predicates, in Ssr style, since keyis 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):Hi Adrian,
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 land l' be two snoc lists without duplicate index, and such that the indexes of l and l'are disjoint, then the concatenation of land 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
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
*)
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: Sep 23 2023 at 15:01 UTC