The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Hi all, some time ago, I tried to do some indenter for proofs inside
coqide, and I was surprised to see that I should manage the Cezar mode
of coq (there is somewhere a "type mode = Mode_none | Mode_proof |
Mode_tactic" in a Decl_mode module).

Some days later I had a tutorial on Isabelle/Isar, so I tried to some
proof in this mode.

As I think that there is not a lot of examples of such scripts,
I send to the list this proof, so any interested person can see how it
works, or use it for a tutorial and I hope that some people will be able
to answer some of my questions.

The proven lemma is that in any separated space[1] all compact space[2]
is closed.

[1]http://en.wikipedia.org/wiki/Hausdorff_space
[2]http://en.wikipedia.org/wiki/Compact_space

>>>
(* copy-pasted from Utf8.v and Utf8_core.v *)
Notation "∀  x .. y , P" := (forall x, .. (forall y, P) ..)
  (at level 200, x binder, y binder, right associativity) : type_scope.
Notation "∃  x .. y , P" := (exists x, .. (exists y, P) ..)
  (at level 200, x binder, y binder, right associativity) : type_scope.
Notation "x ∨ y" := (x \/ y) (at level 85, right associativity) :
type_scope. Notation "x ∧ y" := (x /\ y) (at level 80, right
associativity) : type_scope. Notation "x → y" := (x -> y) (at level 90,
right associativity): type_scope. Notation "x ↔ y" := (x <-> y) (at
level 95, no associativity): type_scope. Notation "¬ x" := (~x) (at
level 75, right associativity) : type_scope. Notation "x ≠ y" := (x <>
y) (at level 70) : type_scope. Notation "'λ'  x .. y , t" := (fun x
=> .. (fun y => t) ..) (at level 200, x binder, y binder, right
associativity). Notation "⊤" := (True).
Notation "⊥" := (False).

(* set ontology *)
Set Implicit Arguments.
Record set (A: Type): Type :=
Comprehension {In: A -> Prop}.

Delimit Scope set_scope with set.
Open Scope set_scope.
Notation "{ x : s 'st' P }" :=
 ({|In:=λ (x: s), P|}) (at level 10, x at level 69): set_scope.
Notation "{ x 'st' P }" := ({x:_ st P}) (at level 10, x at level 69):
set_scope. Notation "x ∈ X" := (X.(In) x) (at level 40): set_scope.
Notation "x ∉ X" := (¬(x ∈ X)) (at level 40): set_scope.
Notation "X ⊆ Y" := (∀ x, x ∈ X → x ∈ Y) (at level 40): set_scope.
Notation "X ≡ Y" := (X⊆Y ∧ Y⊆X) (at level 40): set_scope.
Notation "X ∪ Y" := ({x st x ∈ X ∨ x ∈ Y}) (at level 55): set_scope.
Notation "X ∩ Y" := ({x st x ∈ X ∧ x ∈ Y}) (at level 50): set_scope.
Notation "⋃ X" := ({x st ∃ y, x ∈ y ∧ y ∈ X}) (at level 35): set_scope.
Notation "⋂ X" := ({x st ∀ y, y ∈ X → x ∈ y}) (at level 30): set_scope.
Notation "f ⁻¹ Σ" := ({x st (f x) ∈ Σ}) (at level 5): set_scope.
Notation "∁ A" := ({x st x ∉ A}) (at level 5): set_scope.

Definition empty_set (A: Type) := {x: A st ⊥}.
Definition full_set (A: Type) := {x: A st ⊤}.

Notation "₀ s" := (empty_set s) (at level 5): set_scope.
Notation "₁ s" := (full_set s) (at level 5): set_scope.

Definition finite_union {A: Type} (f: nat -> set A) :=
 fix finite_union n :=
 match n with
 | O => ₀A
 | S k => (f k) ∪ (finite_union k)
 end.

Axiom Extensionnality: ∀ (S: Type) (σ1 σ2: set S), σ1 ≡ σ2 → σ1 = σ2.

Class Topology (S: Type): Type :=
{ O: set (set S);
  Hempty: ₀S ∈ O;
  Hall: ₁S ∈ O;
  Hinter: ∀ ω1 ω2, (ω1 ∈ O) → (ω2 ∈ O) → (ω1 ∩ ω2) ∈ O;
  HUNION: ∀ ωs, (∀ ω, (ω ∈ ωs) → (ω ∈ O)) → (⋃ωs) ∈ O
}.

Definition Compact {A: Type} {ΩA: Topology A} a :=
 ∀ os, (a ⊆ ⋃os ∧ (∀ o, (o ∈ os) → (o ∈ O))) →
 ∃ subos, ∃ n, (∀ m, m<n → (subos m) ∈ os) ∧ a ⊆ (finite_union subos n).

Definition Separables {A: Type} {ΩA: Topology A} x y :=
 ∃ ox, ∃ oy,
 ((y ∈ oy) ∧ (oy ∈ O)) ∧
 ((x ∈ ox) ∧ (ox ∈ O)) ∧
 (ox ⊆ ∁oy). (* equivalent to ((ox∩oy) ≡ ₀A). *)

<<<
Now comes my proof.
>>>

Lemma compacts_are_closed:
 ∀ A {ΩA: Topology A}, (∀ x y, x ≠ y → Separables x y) →
 ∀ a, Compact a → (∁a ∈ O).
proof.
  let A    : Type,
      ΩA   : (Topology A),
      Hsep : (∀ x y, x ≠ y → Separables x y),
      a    : (set A),
      Hcomp: (Compact a).
  claim L1: (∀ out, (out ∉ a) → ∃ opened, (out ∈ opened) ∧
                                          (opened ⊆ ∁a) ∧
                                          (opened ∈ O)).
   let out be such that Hout:(out ∉ a).
   define K as ({s st (s ∈ O) ∧ ∃ t, ((out ∈ t) ∧ (t ∈ O)) ∧ (t ⊆ ∁s)}).
   claim L11: (a ⊆ ⋃K).
    let α be such that Hα:(α ∈ a).
    claim L111: (out≠α).
     assume (out=α).
     hence ⊥ by Hα, Hout.
    end claim.
    then (Separables out α) by Hsep.
    consider open_out, open_α such that Hα1  :(α ∈ open_α)     and
                                        Hα2  :(open_α ∈ O)     and
                                        Hout1:(out ∈ open_out) and
                                        Hout2:(open_out ∈ O)   and
                                        Hdisj:(open_out ⊆ ∁open_α)
    from _fact.
    claim L12: (open_α ∈ K).
     take open_out.
     thus thesis by Hα2, Hout1, Hout2, Hdisj.
    end claim.
    take open_α.
    thus (α ∈ open_α ∧ open_α ∈ K) by Hα1, L12.
   end claim.
   claim L13:(∀ k, (k ∈ K) → (k ∈ O)).
    let k be such that Hk:(k ∈ K).
    thus (k ∈ O) by Hk.
   end claim.
   have (∃ subos, ∃ n, (∀ m, m<n → (subos m) ∈ K) ∧
                       a ⊆ (finite_union subos n))
   by Hcomp, L11, L13.
   consider subK, subK_card such that Hsub:(∀ m, m<subK_card → (subK m)
∈ K)  and Hrec:(a ⊆ (finite_union subK subK_card))
   from _fact.
<<<
Is there any way to directly write something like:

"consider subK, subK_card such that Hsub:(∀ m, m<subK_card → (subK m)
∈ K)  and Hrec:(a ⊆ (finite_union subK subK_card))
   from Hcomp by L11, L13."
rather than what I did or:
"consider subK, subK_card such that Hsub:(∀ m, m<subK_card → (subK m)
∈ K)  and Hrec:(a ⊆ (finite_union subK subK_card))
   from (Hcomp _ (conj L11 L13))."
>>>
   claim L14: (∀ supa, out ∉ supa →
                       supa ⊆ ⋃K →
                       supa ⊆ finite_union subK subK_card →
                       (∀ m : nat, m < subK_card → subK m ∈ K) →
                       ∃ open : set A, out ∈ open ∧
                                       open ⊆ ∁supa ∧
                                       open ∈ O).
<<<
In Isabelle, we can do "per (induction on subK_card, arbitrary a)"
to generalize over a; of course I can do
"escape. generalize dependent a. proof. … end proof.", but I didn't
want to rely on tactics to experiment cezar mode.
>>>
    escape. clear a Hout L11 Hcomp Hrec. proof.
>>>
the previous line is to get rid of some pollution now that we are
generalized
<<<
    per induction on subK_card.
     suppose it is 0.
      let supa : (set A),
          Hout : (out ∉supa),
          Hsupa: (supa ⊆ ⋃K),
          Hfin : (supa ⊆ (₀A)),
          HKinc: (∀ m, m < 0 → subK m ∈ K).
      take (₁A).
      focus on (₁A ⊆ ∁supa).
       let x be such that (x ∈ ₁A) and (x ∈ supa).
       hence ⊥ by Hfin.
      end focus.
      thus (out ∈ ₁A ∧ ₁A ∈ O) by Hall.
     suppose it is (S n) and Hn:thesis for n.
      let supa : (set A),
          Hout : (out ∉supa),
          Hsupa: (supa ⊆ ⋃K),
          Hfin : (supa ⊆ ((subK n) ∪ (finite_union subK n))),
          HKinc: (∀ m, m < S n → subK m ∈ K).
      define suparef as (supa ∩ ∁(subK n)).
      have Hout':(out ∉ suparef) by Hout.
      have Hsupa':(suparef ⊆ ⋃K) by Hsupa.
      have Hfin':(suparef ⊆ finite_union subK n) by Hfin.
      have HKinc':(∀ m, m < n → subK m ∈ K) by le_S, HKinc.
      have HsubK: ((subK n) ∈ K) by le_n, HKinc.
      have (∃ open, out ∈ open ∧ open ⊆ ∁suparef ∧ open ∈ O)
      by (Hn suparef), Hout', Hsupa', Hfin', HKinc'.
      escape.
       clear Hout' Hsupa' Hfin' HKinc' Hn Hout Hsupa Hfin HKinc.
      proof.
<<<
Why an't we do something like:
     "have (out ∉ suparef) by Hout
      and  (suparef ⊆ ⋃K) by Hsupa
      and  (suparef ⊆ finite_union subK n) by Hfin
      and  (∀ m, m < n → subK m ∈ K) by le_S, HKinc
      and  ((subK n) ∈ K) by le_n, HKinc.
      then (∃ open, out ∈ open ∧ open ⊆ ∁suparef ∧ open ∈ O)
      by (Hn suparef)."
So that we won't have to clean after that?
By the way for an unknown reason, you MUST use (Hn suparef),
using Hn alone wont work (infinite loop?).
>>>
      consider out_open such that Hout :(out ∈ out_open) and
                                  Hsupa:(out_open ⊆ ∁suparef) and
                                  Hopen:(out_open ∈ O)
      from _fact.
<<<
Once again, we should not have to do
"have (∃ ...).
 consider ... from _fact."
>>>
      have HsubK_open:((subK n) ∈ O) by HsubK.
      have (∃ out_open', (out ∈ out_open' ∧ out_open' ∈ O) ∧
                         (out_open' ⊆ ∁(subK n)))
      by HsubK.
      consider out_open' such that Hout' :(out ∈ out_open') and
                                   Hopen':(out_open' ∈ O) and
                                   HsubK':(out_open' ⊆ ∁(subK n))
      from _fact.
      take (out_open ∩ out_open').
      focus on (out ∈ (out_open ∩ out_open')).
       thus thesis by Hout, Hout'.
      end focus.
      focus on ((out_open ∩ out_open') ∈ O).
       thus thesis by Hinter, Hopen, Hopen'.
      end focus.
      let o be such that Ho:(o ∈ (out_open ∩ out_open')).
      have (o ∈ out_open) by Ho.
      then Ho1:(o ∉ (supa ∩ ∁(subK n))) by Hsupa.
      have (o ∈ out_open') by Ho.
      then Ho2:(o ∈ ∁(subK n)) by HsubK'.
      assume (o ∈ supa).
      hence ⊥ by Ho1, Ho2.
     end proof. return.
    end induction. end proof. return.
   end claim.
   thus (∃ open : set A, out ∈ open ∧ open ⊆ ∁a ∧ open ∈ O)
   by (L14 a), Hout, L11, Hrec, Hsub.
<<<
Once again L14 alone won't work.
>>>
  end claim.
  claim L2:(⋃{s st ∃ x, (x ∈ s) ∧ (s ⊆ ∁a) ∧ (s ∈ O)} ≡ ∁a).
   focus on (∁a ⊆ ⋃{s st ∃ x : A, x ∈ s ∧ s ⊆ ∁a ∧ s ∈ O}).
    let out be such that (out ∉ a).
    consider opened such that Hout   :(out ∈ opened) and
                              Hopened:(opened ⊆ ∁a ∧ opened ∈ O)
    from (L1 out _hyp).
    take opened.
    thus (out ∈ opened) by Hout.
    take out.
    thus (out ∈ opened ∧ opened ⊆ ∁a ∧ opened ∈ O) by Hout, Hopened.
   end focus.
   let out be such that Hout:(∃ opened, out ∈ opened ∧
                                        (∃ x, x ∈ opened ∧
                                              opened ⊆ ∁a ∧
                                              opened ∈ O)).
   consider opened such that H1:(out ∈ opened) and
                             (∃ x : A, x ∈ opened ∧
                                       opened ⊆ ∁a ∧
                                       opened ∈ O)
   from Hout.
   consider x:A such that (x ∈ opened) and
                       H2:(opened ⊆ ∁a) and
                          (opened ∈ O)
   from _tmp1.
   thus (out ∈ ∁a) by H1, H2.
  end claim.
  claim L3:(∀ ω, (∃ x, x ∈ ω ∧ ω ⊆ ∁a ∧ ω ∈ O) → ω ∈ O).
   let ω:(set A).
   assume H:(∃ x, x ∈ ω ∧ ω ⊆ ∁a ∧ ω ∈ O).
   consider x such that (x ∈ ω) and (ω ⊆ ∁a) and (ω ∈ O) from H.
   hence (ω ∈ O).
  end claim.
  have L4:(⋃{s st ∃ x : A, x ∈ s ∧ s ⊆ ∁a ∧ s ∈ O} ∈ O) by HUNION, L3.
  have (⋃{s st ∃ x : A, x ∈ s ∧ s ⊆ ∁a ∧ s ∈ O} = ∁a) by
Extensionnality, L2. hence (∁a ∈ O) by L4.
 end proof.
Qed.
<<<

As often, it is very surprising that a 4 line proof in manual require
so much lines in Cezar (but also in normal mode, if you do not use
highly automated proofs).

Is this mode "frozen" (with all these flaws) or is it not?