cls-coq/DependentFixpoint.v at master · combinators/cls-coq · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
(* Fix_F with heterogenious type dependent arguments *)

Section DependentFixPoint.
  Variable A: Type.
  Variable R: A -> A -> Prop.
  Variable Rwf: well_founded R.

  Variable T: Type.
  Variable TT: T -> Type.

  Variable P : forall (t: T), TT t -> Type.
  Variable f : forall (t: T), TT t -> A.
  Variable F : forall (t : T),
      forall (x : TT t),
        (forall (t' : T) (y : TT t'),
            R (f t' y) (f t x) -> P t' y) -> P t x.

  Fixpoint Fix_F (t: T) (x: TT t) (a: Acc R (f t x)) : P t x :=
    F t x (fun (t' : T) (y : TT t') (h : R (f t' y) (f t x)) =>
             Fix_F t' y (Acc_inv a h)).

  Definition DepFix (t: T) (x: TT t) := Fix_F t x (Rwf (f t x)).


  Hypothesis
    F_ext :
      forall (t: T) (x: TT t) (g g': forall (t': T) (y: TT t'), R (f t' y) (f t x) -> P t' y),
        (forall (t': T) (y: TT t') (p: R (f t' y) (f t x)), g t' y p = g' t' y p) -> F t x g = F t x g'.

  Fixpoint Fix_F_inv (t: T) (x: TT t) (r s: Acc R (f t x)) { struct r}: Fix_F t x r = Fix_F t x s.
  Proof.
    destruct r.
    destruct s.
    simpl.
    match goal with
    |[|- F t x ?lhs = F t x ?rhs ] =>
     apply (F_ext t x lhs rhs)
    end.
    intros.
    apply Fix_F_inv.
  Qed.

  Definition IsFix (g: forall (t: T) (x: TT t), P t x): Prop :=
    forall t x, g t x = F t x (fun (t' : T) (y : TT t') (h : R (f t' y) (f t x)) => g t' y).

  Fixpoint isFix_unique g (isFix: IsFix g) (t: T) (x: TT t) (acc: Acc R (f t x)) {struct acc}:
    Fix_F t x acc = g t x.
  Proof.
    unfold Fix_F.
    rewrite isFix.
    destruct acc.
    match goal with
    |[|- F t x ?lhs = F t x ?rhs ] =>
     apply (F_ext t x lhs rhs)
    end.
    intros.
    simpl.
    apply isFix_unique.
    exact isFix.
  Qed.
End DependentFixPoint.