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.

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?

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.

Ok, I will think about this.

@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?

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.

I will explain what I mean.

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`

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.

If I run `case a`

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`

(this might not be a good idea in the specific case, it's just a general rule of thumb)

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.

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.

it does make sense.

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).

I ran into problems actually using the lemma above.

I tried to run

```
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?

`clearbody j`

Nice, perfect.

rather than `set (j := _)`

you can use `assert (j := _)`

.

I see, thank you.

Guillaume Melquiond said:

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.

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.

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?

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: Jan 28 2023 at 05:02 UTC