145 lines
3.4 KiB
Coq
145 lines
3.4 KiB
Coq
From Equations Require Import Equations.
|
|
Require Import Autosubst2.core Autosubst2.fintype Autosubst2.syntax
|
|
common typing preservation admissible fp_red structural soundness.
|
|
Require Import algorithmic.
|
|
From stdpp Require Import relations (rtc(..), nsteps(..)).
|
|
Require Import ssreflect ssrbool.
|
|
|
|
Inductive algo_dom {n} : PTm n -> PTm n -> Prop :=
|
|
| A_AbsAbs a b :
|
|
algo_dom a b ->
|
|
(* --------------------- *)
|
|
algo_dom (PAbs a) (PAbs b)
|
|
|
|
| A_AbsNeu a u :
|
|
ishne u ->
|
|
algo_dom a (PApp (ren_PTm shift u) (VarPTm var_zero)) ->
|
|
(* --------------------- *)
|
|
algo_dom (PAbs a) u
|
|
|
|
| A_NeuAbs a u :
|
|
ishne u ->
|
|
algo_dom (PApp (ren_PTm shift u) (VarPTm var_zero)) a ->
|
|
(* --------------------- *)
|
|
algo_dom u (PAbs a)
|
|
|
|
| A_PairPair a0 a1 b0 b1 :
|
|
algo_dom a0 a1 ->
|
|
algo_dom b0 b1 ->
|
|
(* ---------------------------- *)
|
|
algo_dom (PPair a0 b0) (PPair a1 b1)
|
|
|
|
| A_PairNeu a0 a1 u :
|
|
ishne u ->
|
|
algo_dom a0 (PProj PL u) ->
|
|
algo_dom a1 (PProj PR u) ->
|
|
(* ----------------------- *)
|
|
algo_dom (PPair a0 a1) u
|
|
|
|
| A_NeuPair a0 a1 u :
|
|
ishne u ->
|
|
algo_dom (PProj PL u) a0 ->
|
|
algo_dom (PProj PR u) a1 ->
|
|
(* ----------------------- *)
|
|
algo_dom u (PPair a0 a1)
|
|
|
|
| A_UnivCong i j :
|
|
(* -------------------------- *)
|
|
algo_dom (PUniv i) (PUniv j)
|
|
|
|
| A_BindCong p0 p1 A0 A1 B0 B1 :
|
|
algo_dom A0 A1 ->
|
|
algo_dom B0 B1 ->
|
|
(* ---------------------------- *)
|
|
algo_dom (PBind p0 A0 B0) (PBind p1 A1 B1)
|
|
|
|
| A_VarCong i j :
|
|
(* -------------------------- *)
|
|
algo_dom (VarPTm i) (VarPTm j)
|
|
|
|
| A_ProjCong p0 p1 u0 u1 :
|
|
ishne u0 ->
|
|
ishne u1 ->
|
|
algo_dom u0 u1 ->
|
|
(* --------------------- *)
|
|
algo_dom (PProj p0 u0) (PProj p1 u1)
|
|
|
|
| A_AppCong u0 u1 a0 a1 :
|
|
ishne u0 ->
|
|
ishne u1 ->
|
|
algo_dom u0 u1 ->
|
|
algo_dom a0 a1 ->
|
|
(* ------------------------- *)
|
|
algo_dom (PApp u0 a0) (PApp u1 a1)
|
|
|
|
| A_HRedL a a' b :
|
|
HRed.R a a' ->
|
|
algo_dom a' b ->
|
|
(* ----------------------- *)
|
|
algo_dom a b
|
|
|
|
| A_HRedR a b b' :
|
|
ishne a \/ ishf a ->
|
|
HRed.R b b' ->
|
|
algo_dom a b' ->
|
|
(* ----------------------- *)
|
|
algo_dom a b.
|
|
|
|
|
|
Definition fin_eq {n} (i j : fin n) : bool.
|
|
Proof.
|
|
induction n.
|
|
- by exfalso.
|
|
- refine (match i , j with
|
|
| None, None => true
|
|
| Some i, Some j => IHn i j
|
|
| _, _ => false
|
|
end).
|
|
Defined.
|
|
|
|
Lemma fin_eq_dec {n} (i j : fin n) :
|
|
Bool.reflect (i = j) (fin_eq i j).
|
|
Proof.
|
|
revert i j. induction n.
|
|
- destruct i.
|
|
- destruct i; destruct j.
|
|
+ specialize (IHn f f0).
|
|
inversion IHn; subst.
|
|
simpl. rewrite -H.
|
|
apply ReflectT.
|
|
reflexivity.
|
|
simpl. rewrite -H.
|
|
apply ReflectF.
|
|
injection. tauto.
|
|
+ by apply ReflectF.
|
|
+ by apply ReflectF.
|
|
+ by apply ReflectT.
|
|
Defined.
|
|
|
|
|
|
Equations check_equal {n} (a b : PTm n) (h : algo_dom a b) :
|
|
bool by struct h :=
|
|
check_equal a b h with (@idP (ishne a || ishf a)) := {
|
|
| Bool.ReflectT _ _ => _
|
|
| Bool.ReflectF _ _ => _
|
|
}.
|
|
|
|
|
|
(* check_equal (VarPTm i) (VarPTm j) h := fin_eq i j; *)
|
|
(* check_equal (PAbs a) (PAbs b) h := check_equal a b _; *)
|
|
(* check_equal (PPair a0 b0) (PPair a1 b1) h := *)
|
|
(* check_equal a0 b0 _ && check_equal a1 b1 _; *)
|
|
(* check_equal (PUniv i) (PUniv j) _ := _; *)
|
|
Next Obligation.
|
|
simpl.
|
|
intros ih.
|
|
Admitted.
|
|
|
|
Search (Bool.reflect (is_true _) _).
|
|
Check idP.
|
|
|
|
Definition metric {n} k (a b : PTm n) :=
|
|
exists i j va vb, nsteps LoRed.R i a va /\ nsteps LoRed.R j b vb /\
|
|
nf va /\ nf vb /\ size_PTm va + size_PTm vb + i + j <= k.
|
|
|
|
Search (nat -> nat -> bool).
|