CODEWITHSUNDEEP
coqtheorem-provingcoinduction
Bubbler
Bubbler

Reputation: 982

Coq: Proving conat is either finite or infinite

I have a definition of conat which can represent both finite and infinite values, a conversion from nat, a definition of infinity, and a bisimulation relation:

CoInductive conat : Set := O' | S' (n : conat).

Fixpoint toCo (n : nat) : conat := match n with
  | O => O'
  | S n' => S' (toCo n') end.

CoFixpoint inf : conat := S' inf.

CoInductive bisim : conat -> conat -> Prop :=
  | OO : bisim O' O'
  | SS : forall n m : conat, bisim n m -> bisim (S' n) (S' m).

Notation "x == y" := (bisim x y) (at level 70).

I want to prove that conat is either finite or infinite (I'm not 100% sure that this is the correct formulation):

(* This is the goal *)
Theorem fin_or_inf : forall n : conat, (exists m : nat, toCo m == n) \/ (n == inf).

I couldn't prove it so far, but I could prove another statement that, if a conat is not finite, it is infinite (again, not 100% sure about the formulation):

(* I have a proof for this *)
Theorem not_fin_then_inf : forall n : conat, ~ (exists m : nat, toCo m == n) -> (n == inf).

I have no idea how to go from not_fin_then_inf to fin_or_inf though.

  1. Is my definition of fin_or_inf correct?

  2. Can I prove fin_or_inf, either using not_fin_then_inf or not using it?

Also, I found that bridging the gap between the two theorems involves decidability of bisimulation (or extension thereof). I think the decidability theorem could be stated as

Lemma bisim_dec : forall n m : conat, n == m \/ ~ (n == m).
  1. Can I prove bisim_dec or any similar statement on bisimulation?

Edit

The original motivation to prove "either finite or infinite" was to prove commutativity and associativity of coplus:

CoFixpoint coplus (n m : conat) := match n with
  | O' => m
  | S' n' => S' (coplus n' m)
end.
Notation "x ~+ y" := (coplus x y) (at level 50, left associativity).

Theorem coplus_comm : forall n m, n ~+ m == m ~+ n.
Theorem coplus_assoc : forall n m p, n ~+ m ~+ p == n ~+ (m ~+ p).

Going through the same way as nat's + does not work because it requires transitivity of == with a lemma analogous to plus_n_Sm, which makes the cofix call unguarded. Otherwise, I have to destruct both n and m, and then I'm stuck at the goal n ~+ S' m == m ~+ S' n.

If I choose an alternative definition of coplus:

CoFixpoint coplus (n m : conat) := match n, m with
  | O', O' => O'
  | O', S' m' => S' m'
  | S' n', O' => S' n'
  | S' n', S' m' => S' (S' (coplus n' m'))
end.

Then coplus_comm is easy, but coplus_assoc becomes near-impossible to prove instead.

  1. Can I indeed prove coplus_comm with the first definition of coplus, or coplus_assoc with the second?

Upvotes: 4

Views: 281

Answers (0)

Related Questions