Require Import Arith Eqdep_dec.
From Undecidability.Shared Require Import DLW.Utils.utils DLW.Vec.vec DLW.Vec.pos.
From Undecidability.MuRec Require Import recalg.
Set Implicit Arguments.
Set Default Proof Using "Type".
Reserved Notation " '[' f ';' v ']' '-[' n '>>' x " (at level 70).
Inductive ra_ca : forall k, recalg k -> vec nat k -> nat -> nat -> Prop :=
| in_ra_ca_cst : forall n v, [ra_cst n; v] -[ 1 >> n
| in_ra_ca_zero : forall v, [ra_zero; v] -[ 1 >> 0
| in_ra_ca_succ : forall v, [ra_succ; v] -[ 1 >> S (vec_head v)
| in_ra_ca_proj : forall k v j, [@ra_proj k j; v] -[ 1 >> vec_pos v j
| in_ra_ca_comp : forall k i f (gj : vec (recalg i) k) v q w p x,
(forall j, [vec_pos gj j; v] -[ vec_pos q j >> vec_pos w j)
-> [f; w] -[ p >> x
-> [ra_comp f gj; v] -[1+p+vec_sum q>> x
| in_ra_ca_rec_0 : forall k f (g : recalg (S (S k))) v n x,
[f; v] -[ n >> x
-> [ra_rec f g; 0##v] -[ S n >> x
| in_ra_ca_rec_S : forall k f (g : recalg (S (S k))) v n p x q y,
[ra_rec f g; n##v] -[ p >> x
-> [g; n##x##v] -[ q >> y
-> [ra_rec f g; S n##v] -[ 1+p+q >> y
| in_ra_ca_min : forall k (f : recalg (S k)) v x p w q ,
(forall j : pos x, [f; pos2nat j##v] -[ vec_pos q j >> S (vec_pos w j))
-> [f; x##v] -[ p >> 0
-> [ra_min f; v] -[1+p+vec_sum q>> x
where " [ f ; v ] -[ n >> x " := (@ra_ca _ f v n x).
Section inversion_lemmas.
Lemma ra_ca_inv k (f : recalg k) v n x :
[f;v] -[n>> x -> (n = 1 /\ exists (H : k = 0), eq_rect _ _ f _ H = ra_cst x)
\/ (n = 1 /\ x = 0 /\ exists (H : k = 1), eq_rect _ _ f _ H = ra_zero)
\/ (n = 1 /\ exists (H : k = 1), x = S (vec_head (eq_rect _ _ v _ H)) /\ eq_rect _ _ f _ H = ra_succ)
\/ (n = 1 /\ exists p, x = vec_pos v p /\ f = ra_proj p)
\/ (exists i (h : recalg i) gj w q m, n = 1+q+vec_sum m /\ [h;w] -[q>> x
/\ (forall p, [vec_pos gj p;v] -[vec_pos m p>> vec_pos w p)
/\ f = ra_comp h gj)
\/ (exists k' (H : k = S k') (h : recalg k') g m,
n = S m
/\ vec_head (eq_rect _ _ v _ H) = 0
/\ [h;vec_tail (eq_rect _ _ v _ H)] -[m>> x
/\ eq_rect _ _ f _ H = ra_rec h g)
\/ (exists k' (H : k = S k') m y (h : recalg k') g p q,
vec_head (eq_rect _ _ v _ H) = S m
/\ n = 1+p+q
/\ [ra_rec h g; m##vec_tail (eq_rect _ _ v _ H)] -[p>> y
/\ [g; m##y##vec_tail (eq_rect _ _ v _ H)] -[q>> x
/\ eq_rect _ _ f _ H = ra_rec h g)
\/ (exists (g : recalg (S k)) (m w : vec _ x) q,
n = 1+q+vec_sum m
/\ (forall p, [g; pos2nat p##v] -[vec_pos m p>> S (vec_pos w p))
/\ [g; x##v] -[q>> 0
/\ f = ra_min g)
.
Proof.
induction 1 as [ | |
| k v j
| k i f gj v q w p x
| k f g v n x
| k f g v n p x q y
| k f v x p w q
].
do 0 right; left; split; auto; exists eq_refl; auto.
do 1 right; left; do 2 (split; auto); exists eq_refl; auto.
do 2 right; left; split; auto; exists eq_refl; split; simpl; auto.
do 3 right; left; split; auto; exists j; auto.
do 4 right; left; exists k, f, gj, w, p, q; auto.
do 5 right; left; exists k, eq_refl, f, g, n; auto.
do 6 right; left; exists k, eq_refl, n, x, f, g, p, q; auto.
do 7 right; exists f, q, w, p; auto.
Qed.
Local Ltac myinv :=
let H := fresh in
intros H;
apply ra_ca_inv in H;
destruct H as [ (? & ? & ?)
| [ (? & ? & ? & ?)
| [ (? & ? & ? & ?)
| [ (? & ? & ? & ?)
| [ (? & ? & ? & w' & q' & m' & ? & ? & ? & ?)
| [ (? & ? & ? & ? & m' & ? & ? & ? & ?)
| [ (? & ? & ? & y' & ? & ? & p' & q' & ? & ? & ? & ? & ?)
| (? & m' & w' & q' & ? & ? & ? & ?)
] ] ] ] ] ] ].
Ltac injc H := injection H; clear H;
repeat match goal with
|- _ = _ -> _ =>
intro; subst end.
Ltac eqgoal :=
match goal with
|- ?a -> ?b => replace a with b; auto
end.
Ltac inst H :=
let K := fresh in
match goal with
| [ G : ?x -> _ |- _ ] =>
match G with
H => assert (x) as K; [ clear H | specialize (H K); clear K ]
end
end.
Fact eq_gen { X } (P : X -> Type) x : (forall y, y = x -> P y) -> P x.
Proof. intros H; apply H, eq_refl. Qed.
Ltac gen_eq t := apply eq_gen with (x := t).
Fact eq_nat_pirr (n m : nat) (H1 H2 : n = m) : H1 = H2.
Proof. apply UIP_dec, eq_nat_dec. Qed.
Ltac natid :=
repeat
match goal with
| [ H: ?x = ?x :> nat |- _ ] => let G := fresh
in generalize (@eq_nat_pirr _ _ H eq_refl);
intros G; subst H
end;
simpl eq_rect in * |- *.
Local Ltac natSimpl :=
repeat match goal with [ H : S _ = S _ |- _ ] => let G := fresh in injection H; intro G; subst; natid end.
Local Ltac mydiscr :=
repeat match goal with
| H : _ = _ :> nat |- _ => discriminate H; fail
| H : _ = _ :> recalg _ |- _ => discriminate H; fail
end.
Local Ltac myauto := myinv; subst; natid; natSimpl; mydiscr; auto.
Lemma ra_ca_cst_inv i v n x : [ra_cst i;v] -[n>> x -> n = 1 /\ x = i.
Proof. inversion_clear 1; auto. Qed.
Lemma ra_ca_zero_inv v n x : [ra_zero;v] -[n>> x -> n = 1 /\ x = 0.
Proof. inversion_clear 1; auto. Qed.
Lemma ra_ca_succ_inv v n x : [ra_succ;v] -[n>> x -> n = 1 /\ x = S (vec_head v).
Proof. myauto. Qed.
Local Ltac ra_inj :=
match goal with
| H : ra_proj _ = ra_proj _ |- _ => apply ra_proj_inj in H
| H : ra_comp _ _ = ra_comp _ _ |- _ => apply ra_comp_inj in H; destruct H as (? & ? & ?)
| H : ra_rec _ _ = ra_rec _ _ |- _ => apply ra_rec_inj in H; destruct H
| H : ra_min _ = ra_min _ |- _ => apply ra_min_inj in H
end; subst; simpl in * |- *.
Lemma ra_ca_proj_inv k (p : pos k) v n x : [ra_proj p;v] -[n>> x -> n = 1 /\ x = vec_pos v p.
Proof.
myauto; ra_inj; auto.
Qed.
Lemma ra_ca_comp_inv k i f (gj : vec (recalg i) k) v n x :
[ra_comp f gj;v] -[n>> x -> exists p w q,
n = 1+p+vec_sum q
/\ (forall j, [vec_pos gj j;v] -[vec_pos q j>> vec_pos w j)
/\ [f;w] -[p>> x.
Proof.
myauto; ra_inj.
exists q', w', m'; auto.
Qed.
Lemma ra_ca_rec_0_inv k f g v n x :
[@ra_rec k f g; 0##v] -[n>> x -> exists m, n = S m /\ [f;v] -[m>> x.
Proof.
myauto; ra_inj.
exists m'; auto.
Qed.
Lemma ra_ca_rec_S_inv k f g v i n x :
[@ra_rec k f g; S i##v] -[n>> x -> exists y p q,
n = 1+q+p
/\ [ra_rec f g; i##v] -[q>> y
/\ [g; i##y##v] -[p>> x.
Proof.
myauto; ra_inj; natSimpl.
exists y', q', p'; auto.
Qed.
Lemma ra_ca_min_inv k f v n x :
[@ra_min k f;v] -[n>> x -> exists p w q,
n = 1+p+vec_sum q
/\ [f;x##v] -[p>> 0
/\ forall j, [f;pos2nat j##v] -[vec_pos q j>> S (@vec_pos _ x w j).
Proof.
myauto; ra_inj.
exists q', w', m'; auto.
Qed.
End inversion_lemmas.