A solution of the programming problem (Japanese) http://nabetani.sakura.ne.jp/hena/orde09_penwa/

penta.v

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import ZArith Recdef.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive cell := C0 | C1 | C2 | C3.
Inductive dir := D0 | D1 | D2 | D3 | D4.
Definition node := (cell * Z * Z)%type.
Definition link := (cell * Z * Z * dir)%type.
Inductive turn := Cw | Ccw.
Inductive command := Fw | Tn of turn.
Definition action := seq turn.
Definition state := (node * dir)%type.
Definition initial_state : state := ((C0, 0, 0), D0)%Z.

Definition penta_graph c d : link :=
  (match c with
  | C0 => match d with
          | D0 => (C2,  0,  0, D2) | D1 => (C3,  0,  0, D3) | D2 => (C1, -1, -1, D4)
          | D3 => (C3,  0, -1, D0) | D4 => (C1,  0,  0, D1)
          end
  | C1 => match d with
          | D0 => (C2,  0,  0, D3) | D1 => (C0,  0,  0, D4) | D2 => (C2,  0, -1, D0)
          | D3 => (C3,  1,  0, D1) | D4 => (C0,  1,  1, D2)
          end
  | C2 => match d with
          | D0 => (C1,  0,  1, D2) | D1 => (C3,  0,  0, D4) | D2 => (C0,  0,  0, D0)
          | D3 => (C1,  0,  0, D0) | D4 => (C3,  1,  1, D2)
          end
  | C3 => match d with
          | D0 => (C0,  0,  1, D3) | D1 => (C1, -1,  0, D3) | D2 => (C2, -1, -1, D4)
          | D3 => (C0,  0,  0, D1) | D4 => (C2,  0,  0, D1)
          end
  end)%Z.

Definition eqb_cell c1 c2 :=
  match (c1, c2) with
  | (C0, C0) => true | (C1, C1) => true | (C2, C2) => true | (C3, C3) => true | _ => false
  end.

Lemma eqb_cellP : Equality.axiom eqb_cell.
Proof. rewrite /Equality.axiom. by case; case; constructor. Qed.

Canonical cell_eqMixin := EqMixin eqb_cellP.
Canonical cell_eqType := Eval hnf in EqType cell cell_eqMixin.

Definition eqb_dir d1 d2 :=
  match (d1, d2) with
  | (D0, D0) => true | (D1, D1) => true | (D2, D2) => true | (D3, D3) => true | (D4, D4) => true | _ => false
  end.

Lemma eqb_dirP : Equality.axiom eqb_dir.
Proof. rewrite /Equality.axiom. by case; case; constructor. Qed.

Canonical dir_eqMixin := EqMixin eqb_dirP.
Canonical dir_eqType := Eval hnf in EqType dir dir_eqMixin.

Definition eqb_turn t1 t2 := match (t1, t2) with
  | (Cw, Cw) => true | (Ccw, Ccw) => true | _ => false
end.

Lemma eqb_turnP : Equality.axiom eqb_turn.
Proof. rewrite /Equality.axiom. by case; case; constructor. Qed.

Canonical turn_eqMixin := EqMixin eqb_turnP.
Canonical turn_eqType := Eval hnf in EqType turn turn_eqMixin.

Lemma Zeq_boolP : Equality.axiom Zeq_bool.
Proof.
  rewrite /Equality.axiom => x y. case P: (Zeq_bool x y).
    - move/Zeq_bool_eq :P. by constructor.
    - move/Zeq_bool_neq :P. by constructor.
Qed.

Canonical Z_eqMixin := EqMixin Zeq_boolP.
Canonical Z_eqType := Eval hnf in EqType Z Z_eqMixin.

Lemma Zeq_bool_refl x : Zeq_bool x x.
Proof. rewrite /Zeq_bool. elim: x => //=; elim => //=. Qed.

Lemma Z_sub_add x y : (x + -y + y = x)%Z.
Proof. by rewrite Z.add_opp_r Z.sub_add. Qed.

Lemma Z_add_sub x y : (x + y + -y = x)%Z.
Proof. by rewrite Z.add_opp_r Z.add_simpl_r. Qed.

Definition eqb_command a1 a2 := match (a1, a2) with
  | (Fw, Fw) => true | (Tn Cw, Tn Cw) => true | (Tn Ccw, Tn Ccw) => true | _ => false
end.

Lemma eqb_commandP : Equality.axiom eqb_command.
Proof.
  rewrite /Equality.axiom. by case; [|case]; case; [|case| |case| |case]; constructor.
Qed.

Canonical command_eqMixin := EqMixin eqb_commandP.
Canonical command_eqType := Eval hnf in EqType command command_eqMixin.

Definition turn_dir_ccw d : dir :=
  match d with
  | D0 => D1 | D1 => D2 | D2 => D3 | D3 => D4 | D4 => D0
  end.

Definition turn_dir_cw d : dir :=
  match d with
  | D0 => D4 | D1 => D0 | D2 => D1 | D3 => D2 | D4 => D3
  end.

Definition move_ccw (s : state) : state :=
  let: (n, d1) := s in let: d2 := turn_dir_ccw d1 in (n, d2).

Definition move_cw (s : state) : state :=
  let: (n, d1) := s in let: d2 := turn_dir_cw d1 in (n, d2).

Definition move_forward (s : state) : state :=
  let: ((c1, x, y), d1) := s in
  let: (c2, dx, dy, d2) := penta_graph c1 d1 in
  ((c2, x + dx, y + dy), d2)%Z.

Function split_action (cs : seq command) : option (action * seq command) :=
  match cs with
    | [::] => None
    | Fw :: cs1 => Some ([::], cs1)
    | Tn t :: cs1 =>
      match split_action cs1 with
        | None => None
        | Some (ts, cs2) => Some (t :: ts, cs2)
      end
  end.

Lemma split_action_size cs1 cs2 a :
  split_action cs1 = Some (a, cs2) -> size cs1 = size a + size cs2 + 1.
Proof.
  elim: cs1 cs2 a => // c cs1 IHcs1 cs2 a H0. elim: c H0 => /=.
    - case => <- -> /=. by rewrite -addn1.
    - move H0: (split_action cs1) => x. case: x H0 => //.
      move=> x H0 t. case: x H0 => a1 cs H0. case=> H1 H2.
      move/IHcs1 :H0. rewrite -H1 H2 => /= ->. ring.
Qed.

Definition length_order {A} (ls1 ls2 : seq A) := size ls1 < size ls2.

Function convert_to_actions (cs : seq command) {measure size cs} : seq action :=
  match split_action cs with
  | None => [::]
  | Some (a, cs') => a :: convert_to_actions cs'
  end.
Proof.
  move=> cs1 p a cs2 H0. move/split_action_size => ->. apply/ltP.
  by rewrite [size a + size cs2]addnC -addnA -{1}[size cs2]addn0 ltn_add2l addn1 ltn0Sn.
Qed.

Function perform_action s a :=
  match a with
    | Cw :: a' => perform_action (move_cw s) a'
    | Ccw :: a' => perform_action (move_ccw s) a'
    | [::] => move_forward s
  end.

Fixpoint process' s aa :=
  s :: match aa with
    | [::] => [::]
    | a :: aa' => process' (perform_action s a) aa'
  end.

Lemma process'_cons s a aa : process' s (a :: aa) = s :: process' (perform_action s a) aa.
Proof. done. Qed.

Lemma process'_head s aa1 : exists aa2, process' s aa1 = s :: aa2.
Proof.
  rewrite /process'. case: aa1.
  - by exists [::].
  - rewrite -/process'. move=> a aa1. by exists (process' (perform_action s a) aa1).
Qed.

Definition compare_by_node (s1 s2 : state) := fst s1 == fst s2.

Section findo.

Variable T : Type.
Variable a : pred T.

Fixpoint findo' s i := if s is x :: s' then (if a x then Some i else findo' s' i.+1) else None.

Definition findo s := findo' s 0.

Lemma findo'_index s i j : findo' s i = Some j -> i <= j.
Proof.
  elim: s i j => //= x s IHs i j. case: (a x).
  - by case=> ->.
  - move/IHs => H0. rewrite leq_eqVlt. apply/orP. by right.
Qed.

Lemma findo'_head x s i : findo' (x :: s) i = Some i -> a x.
Proof.
  case H0: (a x) => //=. move: H0 => ->. elim: s i => //= x1 s IHs i. case: (a x1).
  - case. move/eqP. by rewrite -addn1 -{2}[i]addn0 eqn_add2l.
  - move/findo'_index. by rewrite -addn1 -{2}[i]addn0 ltn_add2l.
Qed.

Lemma findo'_cons_spec_1 s i j : findo' s j.+1 = Some i.+1 -> findo' s j = Some i.
Proof. elim: s i j => //= x s IHx i j. case: (a x). by case=> ->. apply IHx. Qed.

Lemma findo_cons_spec_1 x s i : findo (x :: s) = Some i.+1 -> a x = false /\ findo s = Some i.
Proof.
  rewrite /findo /findo' -/findo'. case: (a x) => // H0. split => //. move: H0.
  apply findo'_cons_spec_1.
Qed.

Lemma findo'_cons_spec_2 s i j : findo' s j = Some i -> findo' s j.+1 = Some i.+1.
Proof. elim: s i j => //= x s IHx i j. case: (a x). by case=> ->. apply IHx. Qed.

Lemma findo_cons_spec_2 x s i : a x = false /\ findo s = Some i -> findo (x :: s) = Some i.+1.
Proof. rewrite /findo /findo' -/findo'. case=> ->. apply findo'_cons_spec_2. Qed.

Lemma findo_cons_spec x s i : findo (x :: s) = Some i.+1 <-> a x = false /\ findo s = Some i.
Proof. split. apply findo_cons_spec_1. apply findo_cons_spec_2. Qed.

Lemma findo'_cons_head x s i j :
  a x = false -> findo' (x :: s) i = Some j -> exists k, j = k.+1.
Proof.
  rewrite /findo'. move=> ->. rewrite -/findo'. move/findo'_index. case: j => // j _. by exists j.
Qed.

End findo.

Function find_same_node' ss i :=
  match ss with
    | [::] => None
    | s :: ss' =>
      match findo (compare_by_node s) ss' with
        | Some j => Some (i + j + 1, i)
        | None => find_same_node' ss' i.+1
      end
  end.

Definition find_same_node ss := find_same_node' ss 0.

Lemma find_same_node'_index ss i j k : find_same_node' ss i = Some (k, j) -> i <= j.
Proof.
  elim: ss i j k => //= s ss IHss i j k. case: (findo (compare_by_node s) ss).
  - by move=> l [] _ ->.
  - move/IHss => H0. rewrite leq_eqVlt. apply/orP. by right.
Qed.

Lemma find_same_node'_head s1 s2 ss i :
  find_same_node' (s1 :: s2 :: ss) i = Some (i.+1, i) -> compare_by_node s1 s2.
Proof.
  simpl. move H0: (findo (compare_by_node s1) (s2 :: ss)) => o1. case: o1 H0.
  - move=> j H0. case. move/eqP. rewrite -[i.+1]addn1 -addnA eqn_add2l -{2}[1]add0n eqn_add2r.
    move/eqP => H1. rewrite H1 /findo in H0. by move :(findo'_head H0).
  - move=> H0. case (findo (compare_by_node s2) ss).
    + move=> j [] H1. move/eqP. by rewrite -addn1 -{2}[i]addn0 eqn_add2l.
    + move/find_same_node'_index. by rewrite -[i.+1]addn1 -{2}[i]addn0 ltn_add2l.
Qed.

Lemma find_same_node'_head_false s1 s2 ss i j :
  find_same_node' (s1 :: s2 :: ss) i = Some (i + j.+2, i) -> compare_by_node s1 s2 = false.
Proof.
  simpl. move H0: (findo (compare_by_node s1) (s2 :: ss)) => o1. case: o1 H0.
  - move=> k H0. case. move/eqP. rewrite -addnA addn1 eqn_add2l eqSS. move/eqP => H1.
    rewrite H1 in H0. move/findo_cons_spec :H0 => [] H0 H2. apply H0.
  - move=> H0. case: (findo (compare_by_node s2) ss).
    + move=> k [] H1 /eqP. by rewrite -addn1 -{2}[i]addn0 eqn_add2l.
    + move/find_same_node'_index. by rewrite -[i.+1]addn1 -{2}[i]addn0 ltn_add2l.
Qed.

Lemma find_same_node'_cons s1 s2 ss i j :
  compare_by_node s1 s2 = false ->
  find_same_node' (s1 :: s2 :: ss) i = Some (j, i) ->
  find_same_node' (s1 :: ss) i.+1 = Some (j, i.+1).
Proof.
  move=> H0. rewrite /find_same_node' -/find_same_node'.
  move H1: (findo (compare_by_node s1) (s2 :: ss)) => o1. case: o1 H1.
  - move=> k H1 []. move: (findo'_cons_head H0 H1) => [] l H2. rewrite H2 in H1.
    move: (findo_cons_spec_1 H1) => [H3 H4]. rewrite H2 H4. move=> <-.
    congr (Some (_, _)). ring.
  - move=> H1. case (findo (compare_by_node s2) ss).
    + move=> n [] H2 H3. move/eqP :H3. by rewrite -{2}[i]addn0 -addn1 eqn_add2l.
    + move/find_same_node'_index. by rewrite -{2}[i]addn0 -[i.+1]addn1 ltn_add2l.
Qed.

Definition solve' cs s n := find_same_node' (process' s (convert_to_actions cs)) n.

Definition solve cs := solve' cs initial_state 0.

Inductive next_command : seq command -> action -> seq command -> Prop :=
  | NextCommand1 : forall cs, next_command (Fw :: cs) [::] cs
  | NextCommand2 : forall cs1 cs2 t ts, next_command cs1 ts cs2 -> next_command (Tn t :: cs1) (t :: ts) cs2.

Lemma next_command_spec cs1 cs2 a : next_command cs1 a cs2 -> map Tn a ++ Fw :: cs2 = cs1.
Proof.
  elim: a cs1.
    - move=> cs1 H0. by inversion H0; subst => /=.
    - move=> t ts IHa cs1 H0 /=. inversion H0; subst. congr (_ :: _). by apply IHa.
Qed.

Lemma split_action_spec cs1 cs2 a : split_action cs1 = Some (a, cs2) -> next_command cs1 a cs2.
Proof.
  rewrite /split_action. elim: cs1 a => // c cs1. rewrite -/split_action.
  move=> IHcs1 a. elim: c.
    - case => <- ->. constructor.
    - move H0: (split_action cs1) => p. case: p H0 => // p H0 t.
      case: p H0 => a1 cs3 H0. case=> H1 H2. rewrite -H1. constructor.
      apply IHcs1. rewrite -H2. apply H0.
Qed.

Inductive same_node : state -> state -> Prop :=
  | SameNode : forall n d1 d2, same_node (n, d1) (n, d2).

Lemma compare_by_node_spec s1 s2 : compare_by_node s1 s2 <-> same_node s1 s2.
  split.
  - rewrite /compare_by_node. case: s2 => n2 d2. case: s1 => n1 d1 /=. move/eqP => ->. constructor.
  - case=> n d1 d2. rewrite /compare_by_node => /=. done. 
Qed.

Inductive is_answer_2 : state -> nat -> state -> seq command -> nat -> Prop :=
  | IsAnswer21 : forall cs s1 s2 n, same_node s1 s2 -> is_answer_2 s1 n s2 cs n
  | IsAnswer22 : forall cs2 cs3 s1 s2 s3 a n2 n3 n4,
      next_command cs2 a cs3 -> R_perform_action s2 a s3 -> n3 = n2.+1 ->
      is_answer_2 s1 n3 s3 cs3 n4 -> is_answer_2 s1 n2 s2 cs2 n4.

Inductive is_answer_1 : state -> seq command -> nat -> nat -> nat -> Prop :=
  | IsAnswer11 : forall cs1 cs2 s1 s2 a n1 n2 n3, next_command cs1 a cs2 ->
      R_perform_action s1 a s2 -> n2 = n1.+1 -> is_answer_2 s1 n2 s2 cs2 n3 ->
      is_answer_1 s1 cs1 n1 n1 n3
  | IsAnswer12 : forall cs1 cs2 s1 s2 a n1 n2 n3 n4, next_command cs1 a cs2 ->
      R_perform_action s1 a s2 -> n2 = n1.+1 -> is_answer_1 s2 cs2 n2 n3 n4 ->
      is_answer_1 s1 cs1 n1 n3 n4.

Inductive is_answer : seq command -> nat -> nat -> Prop :=
  | IsAnswer cs m n : is_answer_1 initial_state cs 0 m n -> is_answer cs m n.

Lemma find_same_node'_is_answer_2 cs s1 s2 acs i j :
  R_convert_to_actions cs acs ->
  find_same_node' (s1 :: process' s2 acs) i = Some (i + j.+1, i) ->
  is_answer_2 s1 i.+1 s2 cs (i + j.+1).
Proof.
  elim: j cs s1 s2 acs i.
  - move=> cs s1 s2 acs i H0. move: (process'_head s2 acs) => [] ss ->.
    rewrite addn1. move/find_same_node'_head/compare_by_node_spec. apply IsAnswer21.
  - move=> j IHj cs s1 s2 acs i. case: acs.
    + simpl. rewrite /findo /findo'. case: (compare_by_node s1 s2) => // _ [] /eqP.
      rewrite addn0. by rewrite eqn_add2l.
    + move=> ac2 acs2 H0. rewrite process'_cons. move H1: (perform_action s2 ac2) => s3.
      move=> H2. move: (find_same_node'_head_false H2) => H3.
      move/(find_same_node'_cons H3) :H2 => H2.
      inversion H0; subst. move: H2. move H1: (perform_action s2 ac2) => s3.
      rewrite -{1}[j.+2]add1n {1}addnA addn1 => H2. move: (IHj cs' s1 s3 acs2 i.+1 H7 H2).
      rewrite -{2}[i.+1]addn1 -addnA add1n. have H8: i.+2 = i.+2. done. move :H8.
      move/esym :H1 => H1.
      move/R_perform_action_correct :H1. move/split_action_spec :H6. apply IsAnswer22.
Qed.      

Lemma find_same_node'_is_answer_1 cs ss s k m n :
  R_convert_to_actions cs ss -> find_same_node' (process' s ss) k = Some (n, m) ->
  is_answer_1 s cs k m n.
Proof.
  elim: ss cs s k m n => //= a ss IHss cs s k m n H0. inversion H0; subst.
  move H5: (perform_action s a) => s2.
  move H6: (findo (compare_by_node s) (process' s2 ss)) => o. case: o H6.
  - move=> i H6 [] <- <-.
    have H7: is_answer_2 s k.+1 s2 cs' (k + i + 1).
    + have H8: find_same_node' (s :: process' s2 ss) k = Some (k + i + 1, k).
      rewrite /find_same_node'. by rewrite H6.
      move: H8. move: H4. rewrite -addnA addn1. apply find_same_node'_is_answer_2.
    + move: H7.
      have H7: k.+1 = k.+1. done. move: H7. move/esym :H5 => H5.
      move/R_perform_action_correct :H5. move/split_action_spec :H3. apply IsAnswer11.
  - move=> H6 H7. move: (IHss _ _ _ _ _ H4 H7). have H8: k.+1 = k.+1. done. move: H8.
    move/esym :H5 => H5. move/R_perform_action_correct :H5. move/split_action_spec :H3.
    apply IsAnswer12.
Qed.

Lemma solve_spec' cs s k m n : solve' cs s k = Some (n, m) -> is_answer_1 s cs k m n.
Proof.
  rewrite /solve'. move H0: (convert_to_actions cs) => ss1. move/esym :H0 => H0.
  case/R_convert_to_actions_correct :H0 => // cs1 a cs2 H0 acs H1 H2.
  move H3: (perform_action s a) => s1. move: (H2) => /=.
  move H4: (findo (compare_by_node s) (process' (perform_action s a) acs)) => o. case: o H4.
  - move=> i H4 [] H5 H6. rewrite -H5 -H6. rewrite process'_cons H3 -H5 -H6 in H2.
    move: H2. rewrite -addnA addn1. move=> H2.
    move: (find_same_node'_is_answer_2 H1 H2). have H7: k.+1 = k.+1. done. move: H7.
    move/esym :H3 => H3. move/R_perform_action_correct :H3. move/split_action_spec :H0.
    apply IsAnswer11.
  - rewrite H3. move=> H4 H5. move: (find_same_node'_is_answer_1 H1 H5).
    have H6: k.+1 = k.+1. done. move: H6. move/esym :H3 => H3. move/R_perform_action_correct :H3.
    move/split_action_spec :H0. apply IsAnswer12.
Qed.

Theorem solve_spec cs m n : solve cs = Some (n, m) -> is_answer cs m n.
Proof.
  move=> H0. constructor. move: H0. rewrite /solve. apply solve_spec'.
Qed.

Theorem penta_graph_consistent s : solve' [:: Fw; Fw] s 0 = Some (2, 0).
Proof.
  case: s => [] [] [] c1 x1 y1 d1. rewrite /solve'.
  repeat (rewrite convert_to_actions_equation /split_action).
  rewrite /process' /perform_action.
  move H0: (move_forward (c1, x1, y1, d1)) => s2. move: s2 H0 => [] [] [] c2 x2 y2 d2 H0.
  move H1: (move_forward (c2, x2, y2, d2)) => s3. move: s3 H1 => [] [] [] c3 x3 y3 d3 H2.
  move: H0 H2.

  case: c1 ; case: d1;
  try (rewrite /move_forward; rewrite /penta_graph;
       case => <- <- <- <-; case=> <- <- <- <-;
       rewrite /find_same_node' /findo /findo' /compare_by_node => /=;
       repeat rewrite Z.add_0_r; repeat rewrite /eq_op => /=;
       repeat (try rewrite Zeq_bool_refl; try rewrite Z.sub_add; try rewrite (Z_sub_add _ 1);
               try rewrite (Z_add_sub _ 1)) => /=;
       congr (Some _)).
Qed.