Patrick Nicodemus (Apr 29 2022 at 07:00): Patrick Nicodemus (Apr 29 2022 at 07:00):I wrote the following code and I was wondering if somebody could take a look at the overall high level approach and suggest any possible improvements, criticisms, stylistic critiques. It took me a long time to write this because there are a lot of details, I would like to see if it's possible to write a much shorter proof.
I can supply the whole context if anyone wants to step through it line by line, I understand that this may be hard to read without context
I am willing to write Ltac to try and do some of it automatically, if somebody could give me some rough hints on what the Ltac script should do. I have been reading today about typeclass inference and it seems very interesting in general but it's not clear to me how I could apply it here to substantially simplify matters.
Proposition stdfinset_wf {n : nat} (P : stdfinset n -> Type) (T : forall k, Decidable (P k))
: ~{ k : stdfinset n & P k } +
{ x : stdfinset n & (P x) /\ (forall x', P x' -> (x.1 <= x'.1))}.
Proof.
induction n. { left. intros [k p].
contradiction (not_lt_n_0 k.1 k.2). }
unshelve refine (let P' := _ : stdfinset n -> Type in _). {
intros [xval xbd]. apply leq_S in xbd. exact (P (xval; xbd)). }
specialize IHn with P'.
refine (let t := IHn _ in _).
induction t as [nn | ss].
- set (N := (n; n_lt_Sn n) : stdfinset n.+1). induction (T N) as [a | b].
+ right. exists N. split. { assumption. }
abstract(intro x';
induction ((complementaryleqsplit _ _ (leq_S_n _ _ x'.2))) as [_ _ or _];
(* or : sum (n < m) (n = m) *)
induction or as [lt | eq];
[ intro Z; contradiction nn; exists (x'.1; lt);
unfold P'; simpl;
now rewrite (ord_eq_if_vals_eq _ _ x') |
intro; rewrite eq; auto with nat]).
+ left. abstract(intros [k pfk];
induction ((complementaryleqsplit _ _ (leq_S_n _ _ k.2))) as [_ _ ork _];
destruct ork;
[ apply nn; exists (k.1;l); unfold P'; now rewrite (ord_eq_if_vals_eq _ _ k) |
apply b; now rewrite (ord_eq_if_vals_eq _ N k)]).
- right. induction ss as [x ab], ab as [a b].
unshelve eapply exist. { exists x.1. set (j:= x.2); simpl in j. auto with nat. }
split.
+ exact a.
+ abstract(simpl; intros; induction x' as [xval' xbd'];
induction (complementaryleqsplit _ _ (leq_S_n _ _ xbd')) as [_ _ orxval _];
destruct orxval as [lt | eq];
[ set (y :=(xval'; lt) : stdfinset n);
specialize b with y; apply b; unfold P'; simpl;
assert ( xbd' = leq_S xval'.+1 n lt) as RW by apply ishprop_leq;
now rewrite <- RW |
rewrite eq; apply leq_S', x.2]).
Defined.
My first reaction is that it is way too long with way too many inductions. If we were not interested in the proof terms, the function would be something as simple as
Fixpoint test n T k {struct k} :=
match k with
| O => inl ...
| S k' =>
match T (n - k) with
| inl _ => inr (existT (n - k) ...)
| inr _ => test n T k'
end
end.
Definition stdfinset_wf n P T := test n T n.
So, there is no reason for your proof to have more than one single induction.
Patrick Nicodemus (Apr 29 2022 at 07:26):Yes, I do agree it is way too long, but I don't know how to shorten it.
I can change all the inductions to destructs. But is there much difference between writing it as a match statement and writing it as a destruct?
Guillaume Melquiond (Apr 29 2022 at 07:30):No, there is usually no difference between refine (match ...) and destruct. (But there is a large difference between induction and destruct.)
But that wasn't really my point. In your proof, you make an induction over n. In the one I propose, the induction is not on n but on a copy k of it.
Patrick Nicodemus (Apr 29 2022 at 07:36):Ok, I will think about this.
Patrick Nicodemus (Apr 29 2022 at 10:44):@Guillaume Melquiond Is this something along the lines of what you meant? I am finding some difficulty in writing the code that does the work first and proving things about it later, is this approach good or idiomatic?
Fixpoint stdfinset_wf_helper1 (n k : nat) {P : stdfinset n.+1 -> Type}
{T : forall k, Decidable (P k)} : { a : stdfinset n.+1 & P a } + Unit :=
match k with
| O => inr tt
| S k' => match (T (n - k'; _ )) with
| inl holds => inl ((n - k'; mixed_trans1 _ _ _ sub_less (n_lt_Sn _)); holds)
| inr _ => stdfinset_wf_helper1 n k'
end
end.
Definition stdfinset_wf_helper2 (n : nat) {P : stdfinset n.+1 -> Type}
{T : forall k, Decidable (P k)} : { k : stdfinset n.+1 & P k } + Unit
:= stdfinset_wf_helper1 n (S n).
Lemma stdfinset_wf_helper3 (n : nat) {P : stdfinset n.+1 -> Type} {T : forall k, Decidable (P k)} :
match stdfinset_wf_helper2 n with
| inl _ => { x : stdfinset n.+1 & (P x) /\ (forall x', P x' -> (x.1 <= x'.1))}
| inr _ => ~{ k : stdfinset n.+1 & P k }
end.
Proof.
also is this the kind of thing that Program is supposed to be used for?
Patrick Nicodemus (Apr 29 2022 at 10:46):I have run into the following problem, after defining the first two functions I returned to trying to prove the original theorem stdfinset_wf in the way it's stated above, that is
Proposition stdfinset_wf {n : nat} (P : stdfinset n -> Type) (T : forall k, Decidable (P k))
: ~{ k : stdfinset n & P k } +
{ x : stdfinset n & (P x) /\ (forall x', P x' -> (x.1 <= x'.1))}.
where I use the helper function to explain what the values are. However I don't know how to prove the correctness properties I want, because I don't know how to analyze its behavior.
Patrick Nicodemus (Apr 29 2022 at 10:48):I will explain what I mean.
Patrick Nicodemus (Apr 29 2022 at 10:49):I try to introduce the term a, by writing set (a := (stdfinset_wf_helper1 n n)). and then I define the basic outputs by case analysis on a.
a := stdfinset_wf_helper1 n n : {a : stdfinset n.+1 & P a} + Unit
Patrick Nicodemus (Apr 29 2022 at 10:50):This is enough to define the values but I don't seem to be able to prove nontrivial properties about a that aren't contained in its type.
Patrick Nicodemus (Apr 29 2022 at 10:51):If I run case a
Paolo Giarrusso (Apr 29 2022 at 10:54):yes, case analysis on a forgets a's definition — a lemma on the helper stdfinset_wf_helper1 might help — and since stdfinset_wf_helper1 is recursive on k, it might be proven by induction on k
Paolo Giarrusso (Apr 29 2022 at 10:55):(this might not be a good idea in the specific case, it's just a general rule of thumb)
Patrick Nicodemus (Apr 29 2022 at 10:56):I get
{a0 : stdfinset n.+1 & P a0} ->
(~ {k : stdfinset n.+1 & P k} +
{x : stdfinset n.+1 & P x * (forall x' : stdfinset n.+1, P x' -> x.1 <= x'.1)})%type
goal 2 (ID 133) is:
Unit ->
(~ {k : stdfinset n.+1 & P k} +
{x : stdfinset n.+1 & P x * (forall x' : stdfinset n.+1, P x' -> x.1 <= x'.1)})%type
but these extra assumptions don't seem to be related to the original term whose behavior I need to analyze.
Patrick Nicodemus (Apr 29 2022 at 10:56):Paolo Giarrusso said:
(this might not be a good idea in the specific case, it's just a general rule of thumb)
ok, thank you.
Patrick Nicodemus (Apr 29 2022 at 10:57):it does make sense.
Patrick Nicodemus (Apr 29 2022 at 12:54):I rewrote the code to make use of a helper function. Is this a good approach?
Fixpoint stdfinset_wf_helper1 (n k : nat) {P : stdfinset n.+1 -> Type}
{T : forall k, Decidable (P k)} : { a : stdfinset n.+1 & P a } + Unit :=
match k with
| O => inr tt
| S k' => match (T (n - k'; _ )) with
| inl holds => inl ((n - k'; mixed_trans1 _ _ _ sub_less (n_lt_Sn _)); holds)
| inr _ => stdfinset_wf_helper1 n k'
end
end.
Lemma on_stdfinset_wf_helper1 (n : nat) {P : stdfinset n.+1 -> Type}
{T : forall k, Decidable (P k)} :
forall k :nat, match (stdfinset_wf_helper1 n k) with
| inl a => (forall b : stdfinset n.+1, P b -> (n.+1 - k <= b.1) -> a.1 <= b.1)
| inr _ => (forall b : stdfinset n.+1, P b -> (n.+1 - k > b.1))
end.
Proof.
intro k; induction k. { unfold stdfinset_wf_helper1; simpl. now intros [bval bpf] l. }
unfold stdfinset_wf_helper1; simpl.
case (T (n - k;_)). { auto. }
intro n_nmk.
match goal with
[ |- match ?X n k P T with
| inl a => _
| inr _ => _
end] => set (QQ := X); change QQ with (stdfinset_wf_helper1); clear QQ
end.
set (QQ := stdfinset_wf_helper1 n k) in *. destruct QQ.
+ intros b pb ineq.
assert ( (n.+1 - k <= b) + (n - k = b)) as L. {
case (@or _ _ (complementaryleqsplit _ _ ineq)).
* intro; left.
exact (leq_trans (nataddsub_comm_ineq_lemma n k) l).
* intro. now right.
}
case L.
- intro. apply (IHk _ pb _).
- intro. contradiction n_nmk. set (QQ := (n - k; _));
assert (QQ = b) as RW. { apply ord_eq_if_vals_eq; exact p. } now rewrite RW.
+ intros b pf.
assert ( (n - k > b) + (n - k = b)) as L. {
specialize IHk with b; set (t := IHk pf).
set (z:= i_lt_n_sum_m _ _ _ t).
set (mk:= (@nataddpreserveslt _ _ k t)).
rewrite (natminuspluseq _ _ _) in mk.
apply leq_S_n in mk.
apply (@natsubpreservesleq _ _ k) in mk.
rewrite add_n_sub_n_eq in mk.
case (@or _ _ (complementaryleqsplit _ _ mk)); auto with nat.
} case L.
- trivial.
- intros. contradiction (n_nmk). set (QQ :=(n-k;_)).
assert (QQ = b) as RW. { apply ord_eq_if_vals_eq; exact p. } now rewrite RW.
Qed.
This is fine. And just to be clear, I was not suggesting to use a helper function; I was only suggesting that your whole proof should have the exact same structure as a function that would compute the same thing. But using a helper function is perfectly fine (and avoids using abstract all over the place).
Patrick Nicodemus (Apr 29 2022 at 13:40):I ran into problems actually using the lemma above.
Patrick Nicodemus (Apr 29 2022 at 13:40):I tried to run
Patrick Nicodemus (Apr 29 2022 at 13:42): set (j := on_stdfinset_wf_helper1 n (S n)).
set (a := stdfinset_wf_helper1 n (S n)) in j.
destruct a
but this gave me an illegal abstraction error, it wasn't happy that I was trying to generalize a, because the term j specified that a had to be something in particular. I solved the problem by a workaround where i removed the actual term j from the context and replaced it with a variable j0 having the same type:
generalize j.
intro j0. clear j.
destruct a.
This seems like a weird solution. Is there a better way to do this?
Guillaume Melquiond (Apr 29 2022 at 13:51):clearbody j
Patrick Nicodemus (Apr 29 2022 at 13:52):Nice, perfect.
Li-yao (Apr 29 2022 at 13:54):rather than set (j := _) you can use assert (j := _).
Patrick Nicodemus (Apr 29 2022 at 13:59):I see, thank you.
Patrick Nicodemus (May 15 2022 at 04:08):Guillaume Melquiond said:
No, there is usually no difference between
refine (match ...)anddestruct. (But there is a large difference betweeninductionanddestruct.)
But that wasn't really my point. In your proof, you make an induction overn. In the one I propose, the induction is not onnbut on a copykof it.
Hi Guillame, sorry to necro this old thread, but could you tell me what you mean when you say there is a large difference between induction and destruct? From the documentation it seems the only difference is that induction automatically tries to generate some induction hypotheses as well. I do not really know what kind of effect this has under the hood on the terms generated.
Patrick Nicodemus (May 15 2022 at 04:09):It's clear to me what the difference is when we are talking about the natural numbers.
However, for inductive types which don't have nontrivial recursion in their definitions, like the equality type or a sum type, what is the distinction between them?
Guillaume Melquiond (May 15 2022 at 07:09):Induction hypotheses are not a strong difference. Whether you use destruct or induction, Coq has to generate an induction principle P (except that people usually don't call it that way for destruct). The main difference lies in the generated term: induction produces fix aux v => match v return P v with ... end while destruct produces match v return P v with ... end. It happens that Coq does not generate fix when it sees no use for it, so eventually destruct and induction will produce convertible terms for non-recursive types. Thus, depending on your point of view, it can be either a major or a minor difference. (The difference becomes larger when you consider mutually recursive types.)
Last updated: Oct 03 2023 at 20:01 UTC