The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

Is this (proper) subset relation is well-founded? Based on my understand, I believe the answer is no (and maybe we need more assumptions), but I am happy be proven otherwise.  You can see the complete code [1].

Definition finset (A : Type) := list A.

(* proper subset *)

Definition subset {A : Type} (xs ys : finset A) : Prop :=
 (∀ x, In x xs -> In x ys) ∧
 (List.length xs < List.length ys). (* for proper subset *)

Lemma well_founded_subset {A : Type} : 

(∀ x y : A, {x = y} + {x ≠ y}) -> 

well_founded (@subset A).

Proof.

  intro Hdec.
  unfold well_founded.
  induction a as [| ah al Iha].
  + econstructor;
    intros ? [Hyl Hyr].
    simpl in Hyr; nia.
  + 
    (* Induction Hypothesis peeling *)
    pose proof (Acc_inv  Iha) as Ha.  
    (* transitivity *)
    econstructor;
    intros xt Hx.
    (* I can unfold one more time, but 
      will I get anything meaningful? *)
    econstructor;
    intros yt Hy.
    (* case analysis *)
    destruct (List.In_dec Hdec ah yt) as [Hb | Hb].
    ++  

      (* In ah yt *)
      pose proof (subset_member _ _ _ Hb Hy) as Hc.
    (* 
      ah ∈ xs so I can write 
      xs = xsl ++ [ah] ++ xsr.
      From Hx : subset xt (ah :: al)
      I can infer: subset (xsl ++ xsr) al.
      But there is no way I can establish:
      subset yt (xsl ++ xsr) for transitive and 
      induction hypothesis to work.

      My conclusion is: it's not provable but 
      happy to be proven wrong.

      If it's not provable, can we make subset relation 
      well founded? 

    *)
    admit.
  ++ admit.
Admitted.

Best, 

Mukesh

[1] 

https://gist.github.com/mukeshtiwari/ecdebdae6f28ddf4b231d160b16de37d