More example

[jeehoonkang]

WIP

Require Import sflib.

Goal True.
done.
Qed.

Goal exists n, n * n = 9.
eexists.
(* edone. *)
Abort.

Goal forall x (Hx: Some x = Some 1), x = 3.
intros. clarify.
Abort.

Goal forall x (Hx: Some x = Some 1), x = 3.
intros. hinv Hx.
Abort.

Goal forall x (Hx: Some x = Some 1), x = 3.
intros. simpls. ins.
Abort.

Variable rel: forall (a b:nat), Prop.
Inductive relstar: forall (a b:nat), Prop :=
| relstar_refl a: relstar a a
| relstar_one a b
              (AB: rel a b):
    relstar a b
| relstar_trans a b c
                (AB: relstar a b)
                (BC: relstar b c):
    relstar a c
.

Lemma relstar_inv a c (AC: relstar a c):
  a = c \/
  exists b, rel a b /\ relstar b c.
Proof.
  admit.
Qed.

Goal forall a c (AC: relstar a c), a = c.
Proof.
  intros. apply relstar_inv in AC. destruct AC.
  - auto.
  - destruct H. destruct H. admit.
Qed.

Lemma relstar_inv' a c (AC: relstar a c):
  <<AC: a = c>> \/
  exists b, <<AB: rel a b>> /\ <<BC: relstar b c>>.
Proof.
  admit.
Qed.

Goal forall a c (AC: relstar a c), a = c.
Proof.
  intros. apply relstar_inv' in AC. des.
  - auto.
  - admit.
Qed.

(* TODO: hdes? *)

Goal forall a c (AC: relstar a c), a = c.
Proof.
  intros. hexploit relstar_inv'.
  - eauto.
  - intro. des.
Abort.

(* TODO: guard? *)

Goal forall (a b c:nat), a = b /\ b = c /\ c = a.
Proof.
  intros. splits.
Abort.

(* TODO: ii, rr, ... *)

Goal forall (a b c:nat), a = b /\ c = c /\ c = a.
Proof.
  intros. splits; [|M|]; Mdo reflexivity.
Restart.
  intros. splits; [M| |M]; Mskip reflexivity.
Abort.

Goal exists n, n * n = 9.
eexists. eadmit.
Abort.