I am stuck with such proof. The current goal has some strange structure that doesn't allow me to do anything.

```
Require Import Utf8 List Lia.
Set Implicit Arguments.
Axiom ProofIrrelevance: ∀ {P: Prop} (p q: P), p = q.
Definition set A := A → Prop.
Tactic Notation "transparent" "assert" "(" ident(H) ":" open_constr(type) ")" :=
refine (let H := (_: type) in _).
Definition fin n := { i | i < n }.
Structure bijection (A B: Type) := {
bijection_f: A → B;
bijection_g: B → A;
bijection_property_1: ∀ x, bijection_g (bijection_f x) = x;
bijection_property_2: ∀ x, bijection_f (bijection_g x) = x
}.
Definition finite A n := bijection A (fin n).
Definition finite_set {A} (X: set A) n := bijection {x | X x} (fin n).
Fixpoint distinct_elements {A} (L: list A): Prop :=
match L with
| nil => True
| cons x t => ¬ In x t ∧ distinct_elements t
end.
Definition list_of_set {A} (L: list A) (X: set A): Prop :=
distinct_elements L ∧ (∀ x, X x ↔ In x L).
Theorem finite_list_thm {A} {X: set A} {n: nat} (H: finite_set X n):
{ L | list_of_set L X ∧ length L = n }.
Proof.
revert X H. induction n; intros.
+ destruct H. exists nil. compute. intuition. destruct (bijection_f0 (exist _ _ H)). abstract lia.
+ destruct H. assert (n < S n) by auto.
remember (bijection_g0 (exist _ n H)) as W. destruct W as [a H0].
pose (λ x, X x ∧ a ≠ x). pose proof (IHn P). unfold P in *. clear IHn P.
assert (finite_set (λ x, X x ∧ a ≠ x) n).
{ refine (Build_bijection _ _ _ _). Unshelve.
3:{ intros [x [H1 H2]]. assert (exist (λ w, X w) a H0 ≠ exist (λ w, X w) x H1) by abstract congruence.
remember (bijection_f0 (exist _ x H1)) as W0. destruct W0.
assert (exist (λ w, w < S n) x0 l ≠ exist (λ w, w < S n) n H) by abstract congruence.
assert (x0 ≠ n).
{ intuition. subst. apply H4. f_equal. apply ProofIrrelevance. }
exists x0. abstract lia. }
3:{ intros [x H1]. assert (x < S n) by auto. remember (bijection_g0 (exist _ x H2)) as W0.
destruct W0. exists x0. split; auto. assert (x ≠ n) by abstract lia. intro. subst.
assert (H0 = x1) by apply ProofIrrelevance. subst. abstract congruence. }
+ intros [x [H1 H2]]. simpl.
Admitted.
```

I can't destruct anything, can't simplify the goal, can't anything.

Could it be because of using "remember"?

Induction straight off the bat is not the best approach here. Also you might find it easier to separate programs and proofs. To inhabit a sigma type `{x : X | P x}`

, first use a normal `Definition`

to construct `x`

, then prove `P x`

in a separate theorem, and finally wrap it up in the sigma.

Yes, that's the right way to go, I agree. I will do that later.

But still, I'm interested what is possible to do with this current goal with that weird

```
let (x0, p) as s return (s = bijection_f0 (exist (λ x0 : A, X x0) x H1) → fin n) :=
bijection_f0 (exist (λ x0 : A, X x0) x H1) in
λ HeqW0 : exist (λ i : nat, i < S n) x0 p = bijection_f0 (exist (λ x1 : A, X x1) x H1)
```

in it.

I think the only way to make progress is to factor/abstract the goal somehow so you can destruct something, but that's just messier and no less work than refactoring your definitions.

Yes, it's probably messy etc., but the annoying need to see how it's done is still here. :| And refactoring doesn't help much as I still have the same problem with `remember`

.

Why using `remember`

causes such monstrosity inside the goal later? Can I use something else instead of `remember`

, maybe?

I'd say the problem is less with remember and more with "complex dependent types", which don't appear in the plan @Li-yao proposed.

From another point-of-view: with a sigma type, you're defining a function and doing proofs about it. Hence, you are reasoning about the proof term representing the function. This is easier if the proof term is something that you write explicitly in Gallina.

Using tactics to write programs (as opposed to proofs) means your proofs must care about the implementation details of the tactic output.

But to answer your question: in a Gallina program you'd use let; using refine to write let should give that output. The set tactic might also give ou something similar.

Lessness has marked this topic as resolved.

Thank you both for your answers!

I managed to prove my version with the "complex dependent types". Conclusion was that it's better provide witness for the "exists ..." at the beginning and use `remember`

after that.

Last updated: Jun 16 2024 at 01:42 UTC