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.
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.
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).
Right that makes more sense.
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).
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))
?
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
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
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_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.
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?
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 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
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
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).
especially if you're happy with a proof-irrelevance axiom.
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