✔ Stuck with a proof · Coq users

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.

Lessness (Mar 21 2022 at 11:30):

Li-yao (Mar 21 2022 at 13:31):

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.

Lessness (Mar 22 2022 at 14:09):

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)

Li-yao (Mar 22 2022 at 15:10):

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.

Lessness (Mar 23 2022 at 23:17):

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?

Paolo Giarrusso (Mar 23 2022 at 23:53):

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.

Paolo Giarrusso (Mar 23 2022 at 23:55):

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.

Paolo Giarrusso (Mar 23 2022 at 23:57):

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

Paolo Giarrusso (Mar 23 2022 at 23:59):

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.

Notification Bot (Mar 24 2022 at 18:32):

Lessness (Mar 25 2022 at 12:13):

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.

Stream: Coq users

Topic: ✔ Stuck with a proof

Lessness (Mar 21 2022 at 11:27):