Stream: Coq users

Topic: ✔ Stuck with a proof

view this post on Zulip Lessness (Mar 21 2022 at 11:27):

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

view this post on Zulip Lessness (Mar 21 2022 at 11:30):

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

Could it be because of using "remember"?

view this post on Zulip 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.

view this post on Zulip Lessness (Mar 22 2022 at 14:09):

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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Notification Bot (Mar 24 2022 at 18:32):

Lessness has marked this topic as resolved.

view this post on Zulip Lessness (Mar 25 2022 at 12:13):

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: Feb 01 2023 at 12:30 UTC