sf5.coq

Require Export Poly_J.

Check (2+2=4).
Check (ble_nat 3 2 = false).
Check 2+2.
Check ble_nat.
Check ble_nat 3 2.
Check false.

Check (2+2=5).

Theorem plus_2_2_is_4:
2+2=4.
Proof. reflexivity. Qed.

Check plus_2_2_is_4.

Definition plus_fact : Prop := 2+2=4.
Check plus_fact.

Theorem plus_fact_is_true:
plus_fact.
Proof. reflexivity. Qed.

Check plus_fact_is_true.

Definition strange_prop1 : Prop :=
(2+2=5) -> (99+26=42).

Check strange_prop1.

Definition stranfe_prop2 :=
forall n, (ble_nat n 17 = true) -> (ble_nat n 99 = true).

Definition even (n:nat) : Prop :=
evenb n = true.

Check even.
Check (even 3).
Check (even 4).

Definition even_n__even_SSn (n:nat) : Prop :=
(even n) -> (even (S (S n))).

Definition between (n m o:nat) : Prop :=
andb (ble_nat n o) (ble_nat o m) = true.

Definition teen : nat -> Prop := 
between 13 19.

Definition true_for_zero (P:nat -> Prop):Prop:=
P 0.

Definition true_for_n__true_for_Sn
(P:nat->Prop) (n:nat):Prop :=
P n -> P (S n).

Definition preserved_by_S (P:nat->Prop):Prop:=
forall n', P n' -> P (S n').
Definition true_for_all_numbers (P:nat->Prop)
:Prop := forall n, P n.

Definition our_nat_induction (P:nat->Prop)
:Prop :=
(true_for_zero P) -> (preserved_by_S P)
-> (true_for_all_numbers P).

Inductive good_day : day -> Prop:=
|gd_sat : good_day saturday
|gd_sun : good_day sunday.

Print good_day.
Print good_day_ind.
Check gd_sat.
Check gd_sun.
Check good_day.
Check (good_day saturday).

Theorem gds : good_day sunday.
Proof. apply gd_sun. Qed.

Check gds.
Print gds.

Inductive day_before : day -> day -> Prop:=
|db_tue:day_before tuesday monday
|db_wed:day_before wednesday tuesday
|db_thu:day_before thursday wednesday
|db_fri:day_before friday thursday
|db_sat:day_before saturday friday
|db_sun:day_before sunday saturday
|db_mon:day_before monday sunday.

Inductive fine_day_for_singing : day->Prop:=
|fdfs_any : forall d:day, fine_day_for_singing d.

Theorem fdfs_wed:fine_day_for_singing wednesday.
Proof. apply fdfs_any. Qed.

Check fdfs_wed.
Print fdfs_wed.

Inductive ok_day : day -> Prop :=
|okd_gd : forall d, good_day d -> ok_day d
|okd_before : forall d1 d2, ok_day d2
-> day_before d2 d1 -> ok_day d1.

Definition okdw: ok_day wednesday :=
okd_before wednesday thursday
(okd_before thursday friday
(okd_before friday saturday
(okd_gd saturday gd_sat)
db_sat)db_fri)db_thu.

Theorem okdw':ok_day wednesday.
Proof.
apply okd_before with (d2:=thursday).
apply okd_before with(d2:=friday).
apply okd_before with(d2:=saturday).
apply okd_gd. apply gd_sat.
apply db_sat.
apply db_fri.
apply db_thu.
Qed.

Print okdw'.

Check okd_before.

Definition okd_before2 := forall d1 d2 d3,
ok_day d3 -> day_before d2 d1 
-> day_before d3 d2 -> ok_day d1.

Theorem okd_before2_valid : okd_before2.
Proof.
unfold okd_before2.
intros.
apply okd_before in H0.
apply H0.
apply okd_before in H1.
apply H1.
apply H. Qed.

Definition okd_before2_valid' : 
okd_before2 :=
fun (d1 d2 d3:day) => fun (H:ok_day d3)
=> fun (H0:day_before d2 d1) =>
fun (H1:day_before d3 d2) =>
okd_before d1 d2 (okd_before d2 d3 H H1) H0.

Print okd_before2_valid.

Print okd_before2_valid'.
Print okd_before.

Check day_before.
Check okd_before2.
Check okd_before.

Definition okd_before2_valid'' : 
okd_before2 :=
fun (a:day) (aa:day) (aaa:day) (aaaa:ok_day aaa)
(aaaaa:day_before aa a) (aaaaaa:day_before aaa aa) =>
okd_before a aa (okd_before aa aaa aaaa aaaaaa) aaaaa.

Print okd_before2_valid''.
Print okd_before2.
Print ok_day.
Print day_before.
Print day.
Print okd_before.

(*
カリーハワード対応は，ぜひよく理解したい．

・「:」と「=」の区別
　　「A:B」の意味・・・①AはB型
　　　　　　　　　　　  ②AはBの証明
　　「A=B」の意味・・・省略名をつけただけ
*)


Check nat_ind.

Theorem mult_0_r' : forall n:nat,
n * 0 = 0.
Proof.
apply nat_ind.
Case "O". reflexivity.
Case "S". simpl. intros n IHn.
rewrite IHn. reflexivity. Qed.

Theorem plus_one_r' : forall n:nat,
n + 1 = S n.
Proof.
apply nat_ind.
reflexivity.
intros.
simpl.
rewrite H. reflexivity. Qed.


Inductive yesno: Type :=
| yes: yesno
|no : yesno.

Check yesno.
Check Set.
Check yesno_ind.
Check yesno_rec.
Check yesno_rect.

Inductive rgb:Type :=
|red:rgb
|green : rgb
|blue : rgb.
Check rgb_ind.

Inductive natlist: Type :=
|nnil : natlist
|ncons : nat -> natlist -> natlist.

Check natlist_ind.

Inductive natlist1: Type :=
|nnil1 : natlist1
|nsnoc1 : natlist1 -> nat -> natlist1.

Check natlist1_ind.

(*
 natに対するforallの場所が変わった
*)

Inductive ExSet : Type :=
|con1 : bool -> ExSet
|con2 : nat -> ExSet -> ExSet.

Check ExSet_ind.

Inductive tree (X:Type)  :Type :=
| leaf : X -> tree X
| node : tree X -> tree X -> tree X.
Check tree_ind.

Inductive mytype (X:Type): Type :=
|constr1 : X -> mytype X
|constr2 : nat -> mytype X
| constr3 : mytype X -> nat -> mytype X.

Check mytype_ind.

Inductive foo (X Y:Type) : Type :=
|bar : X -> foo X Y
|baz : Y -> foo X Y
|quux : (nat -> foo X Y) -> foo X Y.

Check foo_ind.

Inductive foo' (X:Type) : Type :=
|C1 : list X -> foo' X -> foo' X
|C2 : foo' X.

Check foo'_ind.

Definition P_m0r (n:nat) : Prop :=
n * 0 = 0.

Definition P_m0r' : nat -> Prop :=
fun n => n * 0 = 0.

Check P_m0r.
Print P_m0r.
Check P_m0r'.
Print P_m0r'.

Theorem mult_0_r'' : forall n:nat,
P_m0r n.
Proof.
apply nat_ind.
Case "n = 0". reflexivity.
Case "n = S n'".
unfold P_m0r.
intros n' IHn'.
simpl.
apply IHn'. Qed.

Inductive ev:nat -> Prop :=
|ev_0 : ev O
|ev_SS : forall n:nat, ev n -> ev (S (S n)).

Print ev.
Print ev_ind.

Theorem four_ev': ev 4.
Proof.
apply ev_SS. apply ev_SS. apply ev_0. Qed.

Check four_ev'.
Print four_ev'.

Definition four_ev : ev 4 :=
ev_SS 2 ( (*ev 2 = *) (ev_SS 0 (ev_0))).

Check four_ev.
Check (ev 4).
Check ev_SS.

Definition ev_plus4 : 
forall n, ev n -> ev (4+n) :=
fun (n:nat) (H: ev n) =>
ev_SS (2+n) (ev_SS n H).

Definition ev_plus4a :
forall n, ev n -> ev (S(S(S(S(n))))) :=
fun (n:nat) (H:ev n) =>
ev_SS (S(S(n))) (ev_SS n H).

Definition ev_plus4' : forall n,
ev n -> ev (4+n).
Proof.
intros.
apply ev_SS. apply ev_SS. apply H. Qed.

Print ev_plus4'.

Theorem double_even : forall n,
ev (double n).
Proof.
intro n.
induction n.
apply ev_0.
simpl. apply ev_SS. apply IHn.
Qed.

Theorem double_even1 : forall n, ev (n+n).
Proof.
intros.
induction n.
apply ev_0.
simpl.
rewrite <- plus_n_Sm.
apply ev_SS.
apply IHn. Qed.

Print double_even.

Print nat_ind.
(*
「nat_ind = 
fun P : nat -> Prop => nat_rect P」
のところはよくわからない
*)

Definition double_even' : forall n,
ev (double n) :=
fun (n:nat) => nat_ind 
((*P : nat -> Prop の証明？*)  (fun (a:nat) => ev (double a)))
((*P 0 の証明*) ev_0)
((* (forall n : nat, P n -> P (S n))の証明*)
(fun (m:nat) (H: ev (double m)) => 
(* ev (double (S m))の証明*)
ev_SS (double m) H
)) n.

Print double_even.

Theorem ev_minus2 : forall n,
ev n -> ev (pred (pred n)).
Proof.
intros n E.
induction E as [|n' E'].
Case "E = ev_0". simpl. apply ev_0.
Case "E = ev_SS n' E'".
simpl. apply E'. Qed.

Theorem ev_minus2' : forall n,
ev n -> ev (pred (pred n)).
Proof.
intros n E.
destruct n.
simpl. apply ev_0.
simpl. 
destruct n.
simpl. apply ev_0.
simpl.
inversion E. apply H0. Qed.

Print even.

Theorem ev_even : forall n,
ev n -> even n.
Proof.
intros n E. induction E as [|n' E'].
Case "E = ev_0".
unfold even. reflexivity.
Case "E=ev_SS n' E'".
unfold even.
unfold even in IHE'.
simpl.
apply IHE'. Qed.

Theorem ev_even' : forall n,
ev n -> even n.
Proof.
intros n.
induction n as [|n'].
intros. unfold even. simpl. reflexivity.
intros.
unfold even.
inversion H.
(*たぶん無理*)
Admitted.

Theorem ev_sum:forall n m,
ev n -> ev m -> ev (n+m).
Proof.
intros.
induction H.
apply H0.
simpl. apply ev_SS. apply IHev. Qed.

Theorem SSev_ev_firsttry : forall n,
ev (S (S n)) -> ev n.
Proof.
intros n E.
destruct E as [|n' E'].
Admitted.

Theorem SSev_even : forall n,
ev (S (S n)) -> ev n.
Proof.
intros n E.
inversion E as [|n' E'].
apply E'. Qed.


Theorem SSSSev_even : forall n,
ev (S(S(S(S n)))) -> ev n.
Proof.
intros.
inversion H.
inversion H1.
apply H3. Qed.

Theorem even5_nonsense :
ev 5 -> 2+2=9.
Proof.
intros.
inversion H.
inversion H1.
inversion H3. Qed.

Print even5_nonsense.

Theorem even1_nonsense :
ev 1 -> 2+2=9.
Proof.
intros.
inversion H.
Qed.

Print even1_nonsense.

Theorem ev_minus2'': forall n,
ev n -> ev (pred (pred n)).
Proof.
intros n E.
inversion E as [|n' E'].
Case "E = ev_0". simpl. apply ev_0.
Case "E = ev_SS n' E'".
simpl. apply E'. Qed.

Print plus.
Locate "_ + _".
Print sum.

Theorem ev_ev_even : forall n m,
ev (n+m) -> ev n -> ev m.
Proof.
intros.
induction H0.
simpl in H. apply H.
apply IHev.
(*simpl in H.*)
apply ev_minus2 in  H.
(*simpl in H.*)
apply H. Qed.

SearchAbout double.
SearchAbout plus.

Theorem ev_plus_plys : forall n m p,
ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
intros.
apply ev_ev_even with (n:=n+n).
assert (H1: n+n+(m+p) = (n+m) + (n+p)). 
rewrite plus_assoc.
rewrite plus_swap.
rewrite plus_assoc.
rewrite plus_assoc.
reflexivity.
rewrite H1.
apply ev_sum. apply H.
apply H0.
rewrite <- double_plus.
apply double_even.
Qed.

Theorem ev_plus_plus' : forall n m p,
ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
intros.
apply ev_ev_even with (n:=n+n).
replace (n+n+(m+p)) with (n+m+(n+p)).
apply ev_sum.
apply H. apply H0. 
(* proof of replace *)
rewrite plus_swap.
rewrite plus_assoc.
rewrite plus_assoc.
rewrite plus_assoc.
reflexivity.
(* proof of "ev (n+n)" *)
rewrite <- double_plus.
apply double_even.
Qed.

SearchAbout (_ + _).
Require Import Omega.

Theorem ev_plus_plus'' : forall n m p,
ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
intros n m p Hnm Hnp.
apply (ev_ev_even (n+m) (m+p)).
replace (n+m+(m+p)) with (m+m+(n+p)).
apply ev_sum.
rewrite <- double_plus.
apply double_even.
apply Hnp.
rewrite plus_swap.
rewrite plus_assoc.
rewrite plus_assoc.
rewrite plus_assoc.
reflexivity.
apply Hnm. Qed.

Theorem ev_plus_plus''' : forall n m p,
ev (n+m) -> ev (n+p) -> ev (m+p).
Proof.
intros n m p H H0.
assert (ev ((n+m)+(n+p))).
apply (ev_sum _ _ H H0).
replace ((n+m)+(n+p)) with ((n+n)+(m+p)) in H1 by omega.
apply ev_ev_even with (n+n) (m+p)  in H1.
apply H1.
replace (n+n) with (double n);[apply double_even|].
rewrite <- double_plus.
(*apply double_even.*) reflexivity. Qed.

(* omega・・・プレスバーガー算術 *)

Inductive MyProp : nat -> Prop :=
|MyProp1 : MyProp 4
|MyProp2 : forall n:nat, MyProp n -> MyProp (4+n)
|MyProp3 : forall n:nat, MyProp (2+n) -> MyProp n.



Theorem MyProp_tem : MyProp 10.
Proof.
apply MyProp3.
simpl.
assert (12=4+8) as H12.
reflexivity.
rewrite H12.
apply MyProp2.
assert (8=4+4). reflexivity.
rewrite H.
apply MyProp2.
apply MyProp1. Qed.

Check 1.
Check nat.
Check Set.
Check (1=2).
Check Prop.
Check MyProp.
Check nat.
Print MyProp_tem.

Theorem MyProp_0 : MyProp 0.
Proof.
apply MyProp3.
apply MyProp3.
apply MyProp1. Qed.
Print MyProp_0.

Theorem MyProp_0' : MyProp 0.
Proof.
constructor.
constructor.
constructor. Qed.

Theorem MyProp_0'' : MyProp 0.
Proof.
do 3 constructor. Qed.

Theorem MyProp_0''' : MyProp 0.
Proof.
do 2 apply MyProp3.
apply MyProp1. Qed.

Theorem MyProp_plustwo:forall n:nat,
MyProp n -> MyProp (S(S(n))).
Proof.
intros n E.
apply MyProp3. apply MyProp2. apply E. Qed.

Theorem MyProp_plustwo':forall n:nat,
MyProp n -> MyProp (S(S(n))).
Proof.
intro n.
induction 1.
{
  constructor. constructor. constructor.
}
{
 constructor. apply IHMyProp.
}
{
 apply H.
}
Qed.

Theorem MyProp_plustwo'':forall n:nat,
MyProp n -> MyProp (S(S(n))).
Proof.
intro n.
induction 1.
{
  constructor. constructor. constructor.
}
{
 constructor. apply IHMyProp.
}
{
 apply H.
}
Qed.


Theorem MyProp_plustwo''':forall n:nat,
MyProp n -> MyProp (S(S(n))).
Proof.
intros.
destruct H.
apply MyProp2. apply MyProp3.
apply MyProp1.
apply MyProp2.
apply MyProp3.
apply MyProp2. apply H.
apply H. Qed.

Theorem MyProp_ev : forall n:nat,
ev n -> MyProp n.
intros n E.
induction E as [|n' E'].
apply MyProp_0.
apply MyProp_plustwo. apply IHE'. Qed.

Print ev_ind.

Theorem MyProp_ev' : forall n:nat,
ev n -> MyProp n.
Proof.
apply ev_ind.
apply MyProp_0.
intros. apply MyProp_plustwo. apply H0. Qed.

Theorem ev_MyProp : forall n:nat,
MyProp n -> ev n.
Proof.
 intros.
 induction H.
 - apply ev_SS. apply ev_SS. now apply ev_0.
 - apply ev_SS. apply ev_SS. now apply IHMyProp.
 - now inversion IHMyProp as [| n' Hen Heqn].
Qed.

Print ev.

Check MyProp1.

Theorem plus_assoc' : forall n m p:nat,
n + (m+p) = (n+m)+p.
Proof.
intros n m p.
induction n as [|n'].
reflexivity.
simpl. rewrite IHn'. reflexivity.
Qed.

Theorem plus_comm' : forall n m:nat,
n+m=m+n.
Proof.
induction n as [|n'].
intros m.
rewrite -> plus_0_r. reflexivity.
intros m.
simpl.
rewrite IHn'.
rewrite <- plus_n_Sm.
reflexivity. Qed.

Theorem plus_comm'': forall n m:nat,
n+m=m+n.
Proof.
induction m as [|m'].
simpl. rewrite plus_0_r. reflexivity.
simpl. rewrite <-IHm'.
rewrite <- plus_n_Sm. reflexivity. Qed.

(*
https://www.cis.upenn.edu/~bcpierce/sf/current/Prop.html
*)

Fixpoint true_upto_n__true_everywhere n (P:nat->Prop) : Prop
:=
match n with
| 0 => forall m, P m
| S n => (P (S n)) -> true_upto_n__true_everywhere n P
end.


Example true_upto_n_example :
(true_upto_n__true_everywhere 3 (fun n => even n))
=(even 3 -> even 2 -> even 1 -> forall m:nat, even m).
Proof.
simpl. reflexivity. Qed.

Check ev_ind.

Theorem ev_even'' : forall n,
ev n -> even n.
Proof.
apply ev_ind.
unfold even. reflexivity.
intros.
unfold even.
apply H0. Qed.

Check list_ind.
Check MyProp_ind.
Check ev_ind.

Theorem ev_MyProp' : forall n:nat,
MyProp n -> ev n.
Proof.
apply MyProp_ind.
apply ev_SS. apply ev_SS. apply ev_0.
intros.
apply ev_SS. apply ev_SS. apply H0.
intros.
inversion H0. apply H2. Qed.

Check ev_ind.

Definition MyProp_ev' : forall n:nat,
ev n -> MyProp n := ev_ind MyProp
MyProp_0 (fun m z => MyProp_plustwo m).

Check MyProp_ind.

Definition ev_MyProp'' : forall n:nat,
MyProp n -> ev n:=
MyProp_ind ev 
(ev_SS 2 (ev_SS 0 ev_0))
(fun (m:nat) (e:MyProp m) (ee:ev m) => 
ev_SS (2+m) (ev_SS m ee))
(fun (m:nat) (e:MyProp (2+m)) (ee: ev (2+m))
=> ev_ev_even 2 m ee (ev_SS 0 ev_0)
)
.

(* inversionはどういう証明オブジェクトに
なってるのか？？*)

Module P.

Inductive p:(tree nat) -> nat -> Prop :=
|c1 : forall n,p (leaf _ n) 1
|c2 : forall t1 t2 n1 n2, p t1 n1 -> 
p t2 n2 -> p (node _ t1 t2)(n1+n2)
|c3: forall t n, p t n -> p t (S n).

(*
nat nがtree tにある葉の数以上の時に
p t nは証明可能
*)

End P.

Inductive pal {X:Type} : list X -> Prop :=
c:forall l, l = rev l -> pal l.

Print rev.

Theorem snoc_app : forall X (l:list X) v,
snoc l v = l ++ [v].
Proof.
intros.
induction l.
simpl. reflexivity.
simpl.
rewrite IHl. reflexivity. Qed.



Theorem app_empty : forall X (l:list X),
l ++ [] = l.
Proof.
intros.
induction l.
reflexivity.
simpl. rewrite IHl. reflexivity. Qed.

Theorem app_assoc : forall X (l m n:list X),
l ++ m ++ n = (l ++ m) ++n.
Proof.
intros.
induction l.
reflexivity. 
simpl. rewrite IHl. reflexivity. Qed.


Theorem rev_append : forall X (l l' :list X),
(rev l) ++ (rev l') = rev (l' ++ l).
Proof.
intros X l.
induction l.
intros.
simpl.
rewrite app_empty. reflexivity.
intros.
assert (H: l' ++ x::l = (l'++[x]) ++ l).
induction l'.
reflexivity.
simpl. rewrite IHl'. reflexivity.
rewrite H.
rewrite <- IHl.
simpl.
rewrite snoc_app.
symmetry.
rewrite <- snoc_app.
rewrite rev_snoc.
assert (H2: x::rev l' = [x] ++ rev l').
reflexivity.
rewrite H2.
rewrite app_assoc. reflexivity. Qed.

Theorem rev_involutive : forall X (l:list X),
rev (rev l ) = l.
Proof.
intros.
induction l. reflexivity.
simpl. rewrite rev_snoc.
rewrite IHl. reflexivity. Qed.


Theorem pal1 X : forall l:list X, pal  (l ++ rev l).
Proof.
intros.
induction l.
simpl.
apply c. reflexivity.
simpl. apply c.
inversion IHl.
simpl.
rewrite snoc_app.
rewrite snoc_app.
rewrite <- rev_append.
rewrite <- rev_append.
assert (H1: rev[x] = [x]).
reflexivity.
rewrite H1.
rewrite rev_involutive.
simpl.
rewrite app_assoc.
reflexivity. Qed.

Theorem pal2 X : forall l:list X, pal l -> l = rev l.
Proof.
intros.
inversion H. apply H0. Qed.

Theorem pal3 X : forall l:list X,
l = rev l -> pal l.
Proof.
apply c. Qed.

(* 「あまりうまくいきません」とあるが? *)


Example pal_example1 : pal [1,2,2,1].
Proof.
apply c. simpl. reflexivity. Qed.


Inductive palindrome X : list X -> Prop :=
| pal_nil : palindrome X []
| pal_singleton : forall v, palindrome X [v]
| pal_snoc : forall l v, palindrome X  l -> 
 palindrome X (v :: (snoc l v)) .

Print palindrome_ind.
Print ev_ind.
Print double_even.

Theorem palindrome1 : forall X l,
palindrome X (l ++ rev l).
Proof.
intros.
induction l.
simpl. apply pal_nil.
simpl. rewrite <- snoc_with_append.
apply pal_snoc. apply IHl. Qed.

Theorem palindrome2 : forall X l,
palindrome X l -> l = rev l.
Proof.
intros.
induction H.
reflexivity.
reflexivity.
simpl.
rewrite rev_snoc.
simpl.
rewrite <- IHpalindrome. reflexivity.
Qed.

Fixpoint cut_last X (l:list X) : list X :=
match l with
| nil => nil
| h::t => match t with
  | _::_ => h::cut_last X t
  | nil => nil
end
end.

Eval simpl in cut_last nat [1,2,3].
Eval simpl in cut_last nat [1,2,3,2,1].

Definition tail X l : list X :=
match l with
| h::t => t
| nil => nil
end.

Definition trim X (l:list X) : list X :=
tail X (cut_last X l).

Theorem snoc_cutlast : forall X l v,
cut_last X (snoc l v) = l.
Proof.
intros.
induction l.
reflexivity.
simpl. rewrite IHl.
remember (snoc l v).
destruct l0.
destruct l. inversion Heql0.
inversion Heql0.
reflexivity.
Qed.

Theorem cons_cutlast : forall X h h' t,
cut_last X (h::h'::t) = h::(cut_last X (h'::t)).
Proof.
intros.
induction t.
reflexivity.
simpl. reflexivity. Qed.

Definition trim' X (l:list X) : list X :=
cut_last X (tail X l) .

Theorem trim_equivalent : forall X l,
trim X l = trim' X l.
Proof.
intros.
induction l.
reflexivity.
simpl.
destruct l.
reflexivity.
unfold trim'.
reflexivity. Qed.



Theorem snoc_tail : forall X h t v,
tail X (snoc (h::t) v) = snoc (tail X (h::t)) v.
Proof.
intros.
induction t.
reflexivity.
simpl.
reflexivity. Qed.


Theorem tail_rev : forall X l, 
tail X (rev l) = rev (cut_last X l).
Proof.
intros.
induction l.
reflexivity.
destruct l.
reflexivity.
rewrite cons_cutlast.
simpl in IHl.
simpl.
rewrite <- IHl.
remember (snoc (rev l) x0).
destruct l0.
destruct (rev l).
inversion Heql0.
inversion Heql0.
rewrite snoc_tail. reflexivity. Qed.

Theorem cutlast_tail : forall X l,
tail X (cut_last X l) = cut_last X (tail X l).
Proof.
intros.
induction l.
reflexivity.
simpl.
destruct l.
reflexivity.
simpl. reflexivity. Qed.


Theorem trim_rev: forall X l,
trim X (rev l) = rev (trim X l).
Proof.
intros.
destruct l.
reflexivity.
simpl.
rewrite trim_equivalent.
unfold trim'.
unfold trim.
rewrite cutlast_tail.
simpl.
rewrite <- tail_rev.
rewrite <- cutlast_tail.
rewrite snoc_cutlast.
reflexivity. Qed.


Theorem revll_trim : forall X l m,
l = rev l -> m = trim X l -> m = rev m.
Proof.
intros.
rewrite H0.
rewrite <- trim_rev.
rewrite <- H. reflexivity. Qed.

Theorem cutlast_rev : forall X l,
cut_last X (rev l) = rev (tail X l).
Proof.
intros.
destruct l.
reflexivity.
simpl.
rewrite snoc_cutlast. reflexivity. Qed.

Theorem rev_cutlast : forall X l,
rev (cut_last X l) = tail X (rev l).
Proof.
intros.
induction l.
reflexivity.
simpl.
destruct l.
reflexivity.
assert (H: rev (x :: cut_last X (x0 :: l)) =snoc (rev (cut_last X (x0 :: l))) x).
reflexivity.
rewrite H.
rewrite IHl.
simpl.
destruct (rev l).
reflexivity.
simpl. reflexivity. Qed.

Definition liat X (l:list X) : list X := cut_last X l.

Fixpoint daeh X (l:list X) : list X :=
match l with
| [] => []
| h::t => match t with
  | [] => [h]
  |h'::t' => daeh X t
end
end.

Definition head X (l:list X): list X :=
match l with
|[] => []
|h::t => [h]
end.

Theorem cons_app : forall X l (x:list X),
x::l = [x] ++ l.
Proof.
intros.
simpl. reflexivity. Qed.

Theorem cons_liat : forall X x1 x2 l,
liat X (x1::x2::l) = x1::(liat X (x2::l)).
Proof.
intros.
simpl.
destruct l. reflexivity.
reflexivity. Qed.

Theorem daeh_cons : forall X x1 x2 l,
daeh X (x1::x2::l) = daeh X (x2::l).
Proof.
intros.
simpl.
reflexivity. Qed.

Theorem liat_daeh : forall X l,
l = (liat X l )++ (daeh X l).
Proof.
intros.
induction l.
reflexivity.
destruct l.
reflexivity.
rewrite cons_liat.
assert (H:(x :: liat X (x0 :: l))=[x] ++ (liat X (x0 :: l))).
reflexivity.
rewrite H.
rewrite <- app_assoc.
rewrite daeh_cons.
rewrite <- IHl.
simpl. reflexivity. Qed.



Theorem head_trim_daeh : forall X (h1 h2:X)  t, 
h1::h2::t = (head X (h1::h2::t)) ++ (trim X (h1::h2::t)) ++ (daeh X (h1::h2::t)).
Proof.
intros.
simpl.
rewrite trim_equivalent.
unfold trim'.
simpl.
destruct t.
simpl.
reflexivity.
assert (H1: (h2 :: cut_last X (x :: t)) = [h2] ++cut_last X (x :: t)).
reflexivity.
rewrite H1.
rewrite <- app_assoc.
assert (H2:cut_last = liat).
reflexivity.
rewrite H2.
rewrite <- liat_daeh. reflexivity. Qed.

Theorem snoc_daeh : forall X l x,
daeh X (snoc l x) = [x].
Proof.
intros.
induction l.
reflexivity.
simpl. rewrite IHl.
destruct (snoc l x).
inversion IHl. reflexivity. Qed.

Theorem rev_daeh : forall X l,
head X l = daeh X (rev  l).
Proof.
intros.
destruct l.
reflexivity.
simpl.
rewrite snoc_daeh. reflexivity. Qed.


Theorem revll_h_trim_h : forall X (l: list X),forall h h' u, l = h::h'::u ->
l = rev l -> forall t, t = trim X l  ->  
l = h::(snoc t h).
Proof.
intros.
rewrite H.
rewrite H1.
rewrite trim_equivalent.
rewrite H.
unfold trim'.
simpl.
destruct u. 
rewrite H in H0.
inversion H0.
reflexivity.
assert (H2: cut_last = liat). reflexivity.
rewrite H2.
rewrite <- cons_liat.
rewrite snoc_app.
rewrite cons_liat.
assert (H3:[h] = daeh X (x::u)).
assert (H4:daeh X (x::u) = daeh X (l)).
rewrite H.
rewrite daeh_cons.
rewrite daeh_cons. reflexivity. rewrite H4.
rewrite H0.
rewrite <- rev_daeh.
rewrite H. reflexivity.
rewrite H3.
assert (H4:h' :: liat X (x :: u) = [h'] ++ liat X (x :: u) ).
reflexivity.
rewrite H4.
rewrite <- app_assoc.
rewrite <- liat_daeh. reflexivity. Qed.


Theorem palindrome_trim: forall X l l',
palindrome X l' ->
l' = trim X l -> l = rev  l -> palindrome X l.
Proof.
intros.
destruct l.
apply pal_nil.
destruct l.
apply pal_singleton.
rewrite revll_h_trim_h with (h:=x)(h':=x0)(u:=l)(t:=l').
apply pal_snoc. apply H.
reflexivity.
rewrite <-H1. reflexivity.
rewrite H0. reflexivity. Qed.

SearchAbout nat.

Theorem length_trim : forall X x x0 l,
length (trim X (x :: x0 :: l)) = length l.
Proof.
intros.
induction l.
reflexivity.
simpl.
rewrite trim_equivalent in IHl.
unfold trim' in IHl.
simpl in IHl.
rewrite <- IHl.
destruct l.
reflexivity.
reflexivity. Qed.

Inductive nat2 : nat -> Prop :=
|nat0 : nat2 0
|nat1: nat2 1
|natSS : forall n, nat2 n-> nat2 (S(S(n))).

Print nat2_ind.

Definition nat2_le n := forall m l, n=m+l -> nat2 l.

Theorem nat2_nat_le : forall n, nat2_le n -> nat2 (S(n)).
Proof.
intros.
destruct n.
apply nat1.
destruct n.
apply natSS. apply nat0.
apply natSS.
apply H with(m:=1).
reflexivity. Qed.

Theorem nat2_len_forall : forall n, nat2_le n.
Proof.
intros.
induction n.
unfold nat2_le.
intros. destruct l. apply nat0.
rewrite plus_comm in H.
simpl in H.
inversion H.
unfold nat2_le in IHn.
unfold nat2_le.
intros.
destruct l.
apply nat0.
destruct l.
apply nat1.
apply natSS.
rewrite plus_comm in H.
simpl in H.
inversion H.
rewrite plus_comm in H1.
apply IHn with (m:=1+m).
rewrite H1. reflexivity. Qed.

Theorem nat2_nat:forall n, nat2 n.
Proof.
intros.
induction n.
apply nat0.
apply nat2_nat_le.
apply nat2_len_forall. Qed.


Print nat2_ind.

Theorem palindrome3': forall X n, nat2 n-> forall l, n = length l -> 
 l = rev  l -> 
palindrome X l.
Proof.
intros X n H.
induction H.
intros.
destruct l. apply pal_nil. inversion H0.
inversion H.
intros.
destruct l. inversion H.
inversion H.
assert (H3:l=nil).
destruct l.
reflexivity. inversion H2.
rewrite H3.
apply pal_singleton.
intros.
destruct l. apply pal_nil.
destruct l. apply pal_singleton.
rewrite revll_h_trim_h with (h:=x)(h':=x0)(u:=l)(t:=trim X (x::x0::l)).
apply pal_snoc.
apply revll_trim with (m:=(trim X (x::x0::l))) in H1.
apply IHnat2.
rewrite length_trim.
inversion H0.
reflexivity.
apply H1.
reflexivity. reflexivity. apply H1. reflexivity. Qed.

Theorem palindrome_converse : forall X l, l = rev l -> palindrome X l.
Proof.
intros.
apply palindrome3' with(n:=length l).
apply nat2_nat.
reflexivity. apply H. Qed.


Inductive subseq X:  list X -> list X -> Prop :=
| subseq_empty : subseq X [] []
| subseq_seq : forall t l, subseq X t l -> forall h, subseq X (h::t) l
| subseq_sub : forall t l, subseq X t l -> forall h, subseq X (h::t) (h::l).

Theorem subseq_reflexive : forall X l, subseq X l l.
Proof.
intros.
induction l.
apply subseq_empty.
apply subseq_sub. apply IHl. Qed.

Theorem app_nil:forall X (l:list X), l ++ [] = l.
Proof.
intros.
induction l. reflexivity.
simpl. rewrite IHl. reflexivity. Qed.

Theorem subseq_app : forall X l2 l1 l3,
subseq X l2 l1 -> subseq X (l2++l3) l1.
Proof.
intros X l2.
induction l2.
intros.
inversion H. 
simpl. 
induction l3.
apply subseq_empty.
apply subseq_seq. apply IHl3.
intros.
simpl.
inversion H.
apply subseq_seq.
apply IHl2. apply H3.
apply subseq_sub. apply IHl2. apply H3. Qed.

Theorem subseq_nil : forall X l,
subseq X l [].
Proof.
intros.
induction l. apply subseq_empty.
apply subseq_seq. apply IHl. Qed.

Theorem subseq_transitive : forall X l3 l1 l2,
subseq X l2 l1 -> subseq X l3 l2 -> subseq X l3 l1.
Proof.
intros X l3.
induction l3.
intros.
inversion H0. rewrite <- H2 in H. apply H.
intros.
inversion H0.
apply subseq_seq. apply IHl3 with(l2:=l2).
apply H. apply H4.
rewrite <- H2 in H0.
rewrite <- H2 in H.
destruct l1.
apply subseq_nil.
inversion H0.
apply subseq_seq. apply IHl3 with(l2:=(x::l)).
apply H. apply H8.
inversion H.
apply subseq_seq. apply IHl3 with (l2:=(l)).
apply H12. apply H6.
apply subseq_sub.
apply IHl3 with (l2:=(l)).
apply H10. apply H6. Qed.


Inductive fooo (X:Set) (Y:Set):Set :=
|foo1 : X -> fooo X Y
|foo2 : Y -> fooo X Y
|foo3 : fooo X Y -> fooo X Y.

Check fooo.
Print fooo_ind.

Check foo1.

Check Type.
Check Prop.
Check Set.

Definition aaa :Type := Prop.
Definition bbb := Type -> Type.
Check bbb.
Definition bbbb := Prop -> Prop.
Check bbbb.
Definition bbbbb:= Set -> Set.
Check bbbbb.
Definition cc:= Set -> Set.
Definition ccc := Set -> Set -> Set.
Check ccc.
Definition cccc := Set -> cc.
Check cccc.
Print cccc.
Theorem cccc_ccc : cccc = ccc.
Proof.
unfold cccc. unfold ccc. unfold cc. reflexivity. Qed.

Check cccc_ccc.
Check (cccc=ccc).
Print cccc_ccc. Print eq_refl.

Theorem cccc_ccc_eq_refl : (cccc_ccc = eq_refl).
Proof. admit. Qed.
Print cccc_ccc_eq_refl.
(* これは証明できない*)

(* Printの引数はFirstorder
Print (cccc=ccc).
*)

Print cccc_ccc_eq_refl.
Check cccc_ccc_eq_refl.
Print cccc_ccc_eq_refl_admitted.


Definition ccccccc := (cccc=ccc).
Print ccccccc.
Check ccccccc.

Theorem ccccccc_cccc_ccc : ccccccc = (cccc=ccc).
Proof. unfold ccccccc. reflexivity. Qed.

Theorem cccc_ccc2 : ccccccc.
Proof. unfold ccccccc. unfold cccc. unfold ccc. unfold cc.
reflexivity. Qed.

Print cccc_ccc2.

Theorem cccc_cccc : cccc_ccc = cccc_ccc2.
Proof.
admit. Qed.
(*証明できない*)

Print cccc_ccc.
Print cccc_ccc2.
Print ccccccc_cccc_ccc.

(*
cccc_ccc = eq_refl
cccc_ccc2 = eq_refl
ccccccc_cccc_ccc = eq_refl
の関係がある．
これらが等しいことは証明できない．

それぞれの型（？）は別
cccc_ccc : (cccc=ccc)
cccc_ccc2 : ccccccc
ccccccc_cccc_ccc : (ccccccc = (cccc = ccc))

「cccc=ccc」を定義に従って証明した（eq_refl）という操作がcccc_ccc
「ccccccc」を定義に従って証明した（eq_refl）という操作がcccc_ccc2
「ccccccc = (cccc = ccc)」を定義に従って証明した（eq_refl）という操作がccccccc_cccc_ccc
*)

Definition d := Set -> Set.
Print d. Check d.

Definition dd := forall x:Set, Set.
Print dd. Check d.

Theorem d_dd : d=dd.
Proof. unfold d. unfold dd. reflexivity. Qed.

Print d_dd.

Check (nil ).

Check (fun x:Set => x).
Check (fun x:Set => Set).   (* Set -> Type *)
Check (fun X : Type => (@nil X)). 

Check (Set:Type).
Check (123:nat).
Check (1=2:Prop).
Check (1=2:Prop:Type).
(*
このような関係はあまり問題にならない？
*)


Definition ddd := forall x:nat, x=x.
Theorem dddd : forall x:nat, x=x.
Proof.
intros. reflexivity. Qed.

Theorem dddd' : ddd.
Proof.
unfold ddd. apply dddd. Qed.

Print ddd.
Print dddd.
Print dddd'.

Theorem ddddd : dddd' = dddd.
Proof.
admit. Qed.

Print ddddd.
Print ddddd_admitted.

Definition dddddd := nat -> Prop.
Definition ddddddd := (fun x:nat => x=x).
Print ddddddd.
Check (ddddddd : dddddd).
Check ddd. Print ddd. Print dddd.

Eval simpl in (dddd 3). (* 「dddd 3」は3=3の根拠 *)
Eval simpl in (ddddddd 3).
Eval compute in (ddddddd 3). 
(*「ddddddd 3」は3=3に簡約されるが，3=3の証明とは関係がない*)
Print ddddddd.
Print dddd.

Definition ddddddd3 := ddddddd 3.
Theorem ddddddd3_proof : ddddddd3.
Proof.
unfold ddddddd3. unfold ddddddd. reflexivity. Qed.

Print ddddddd3_proof.

(* わかりやすい例 *)

(* Definitionは名前をつける *)
(* 「a2+b2=c2」という等式に「Pythagorean_equation」という名前をつける*)
Definition Pythagorean_equation a2 b2 c2 := a2+b2=c2.

(* 「Pythagorean_theorem」という名前をつける *)
Definition Pythagorean_theorem := forall a2 b2 c2, Pythagorean_equation a2 b2 c2.

Definition Pythagorean_theorem345 := forall a2 b2 c2:nat, Pythagorean_equation 3 4 5.

Check Pythagorean_equation.   (* nat -> nat -> Prop *)
Check (Pythagorean_equation 3 4 5).  (* Prop *)
Check Pythagorean_theorem.  (* Prop *)

Theorem Pythagorean_proof : Pythagorean_theorem.
Proof.
unfold Pythagorean_theorem.
intros.
unfold Pythagorean_equation.
admit.
Qed.

Theorem Pythagorean345_proof : Pythagorean_equation 3 4 5.
Proof.
apply Pythagorean_proof. Qed.

Print Pythagorean_proof.
Print Pythagorean_proof_admitted.

Check Pythagorean_proof.
Check Pythagorean_proof_admitted.  
(* Pythagorean_proof_admitted : forall a2 b2 c2 : nat, a2 + b2 = c2 *)
Print Pythagorean_theorem.
(*Pythagorean_theorem = forall a2 b2 c2 : nat, Pythagorean_equation a2 b2 c2 *)
(*　　　　　　　　　　　forallが必要なためforallが出力されている*)
Print Pythagorean_theorem345.
(* Pythagorean_theorem345 = nat -> nat -> nat -> Pythagorean_equation 3 4 5 *)
(*　　　　　　　　　　　　　forallが不要なためforallはない（Definition時はforallがあった）*)

Check Pythagorean_theorem.
Check Pythagorean_theorem345.
Check (nat -> nat).  (* Set *)
Check (nat -> nat -> nat). (* Set *)
Check (nat -> nat -> nat -> Pythagorean_equation 3 4 5).  (* Prop *)
Check nat.

Check Set.
Check (Set -> Set).

Check Pythagorean_theorem.  (* Prop *)

Check Pythagorean_equation. (* nat -> nat -> nat -> Prop *)
Print Pythagorean_theorem. (* forall a2 b2 c2 : nat, Pythagorean_equation a2 b2 c2 *)
(* Pythagorean_theoremの型はPythagorean_equation a2 b2 c2の型と同じ*)
Check Pythagorean_theorem.
Check (Pythagorean_equation 1 2 3).
(* Pythagorean_theoremの型もPythagorean_equation a2 b2 c2の型もProp *)

Print Pythagorean345_proof.

Check Pythagorean_proof.
Print Pythagorean_proof.

Eval simpl in (Pythagorean_proof 3 4 5).
Eval compute in (Pythagorean_proof 3 4 5).
(* Pythagorean_proof_admitted 3 4 5と表示されて欲しかった *)


Inductive baar : Set :=
|bar1 : nat -> baar
|bar2 : baar -> baar
|bar3 :bool -> baar -> baar.

Print baar_ind.

Inductive no_longer_than (X:Set) : (list X) -> nat -> Prop:=
|nlt_nil : forall n, no_longer_than X [] n
|nlt_cons : forall x l n, no_longer_than X l n -> no_longer_than X (x::l) (S n)
|nlt_succ : forall l n, no_longer_than X l n -> no_longer_than X l (S n).

Print no_longer_than_ind.

Inductive R: nat -> list nat -> Prop :=
|c1 : R 0 []
|c2 : forall n l, R n l -> R (S n) (n::l)
|c3 : forall n l, R (S n) l -> R n l.

Theorem R1 : R 2 [1,0].
Proof.
apply c2. apply c2. apply c1. Qed.

Theorem R2 : R 1 [1,2,1,0].
Proof.
apply c3. apply c2. apply c3. apply c3. apply c2. apply c2. apply c2. apply c1. Qed.

(* R 6 [3,2,1,0]は証明できない *)