Inductive val :=
  | VNat (n : nat)
  | VCons (a b : val)
  | VProp (P : Prop).

Definition truth (v : val) : Prop :=
  match v with
  | VProp P => P
  | _ => False
  end.

Fixpoint sem (t : term) (env : var -> val) : val :=
  match t with
  | TVar x => env x
  | TNat n => VNat n
  | TCons a b => VCons (sem a env) (sem b env)
  | FTop => VProp True
  | FBot => VProp False
  | FImp a b => VProp (truth (sem a env) -> truth (sem b env))
  | FEqu a b => VProp (sem a env = sem b env)
  | FAll f => VProp (forall d, truth (sem f (d .: env)))
  | FNot a => VProp (~ truth (sem a env))
  | FAnd a b => VProp (truth (sem a env) /\ truth (sem b env))
  end.

Lemma sem_ext t env env' :
  (forall x, env x = env' x) -> sem t env = sem t env'.
Proof.
  move=> h.
  by have->: env = env' by f_ext.
Qed.

Lemma sem_ren t ξ env :
  sem t.[ren ξ] env = sem t (ξ >>> env).
Proof.
  elim: t ξ env=> //=; try by (move=> ? ih1 ? ih2 *;
                               rewrite ih1 ih2).
  - move=> f ih ξ env.
    f_equal.
    apply forall_extensionalityP=> d.
    asimpl.
    rewrite ih.
    f_equal.
    apply sem_ext=> -[|x]; by asimpl.
  - move=> ? ih *.
    by rewrite ih.
Qed.

Lemma sem_subst t σ env :
  sem t.[σ] env = sem t (fun x => sem (σ x) env).
Proof.
  elim: t σ env=> //=.
  - move=> ? ih1 ? ih2 *.
    by rewrite ih1 ih2.
  - move=> ? ih1 ? ih2 *.
    by rewrite ih1 ih2.
  - move=> ? ih1 ? ih2 *.
    by rewrite ih1 ih2.
  - move=> f ih σ env.
    f_equal.
    apply forall_extensionalityP=> d.
    rewrite ih.
    f_equal.
    apply sem_ext=> -[|x]; first by asimpl.
    asimpl.
    by rewrite sem_ren.
  - move=> ? ih *.
    by rewrite ih.
  - move=> ? ih1 ? ih2 *.
    by rewrite ih1 ih2.
Qed.

Declare Scope model_scope.

Module Model : VALID.

Definition valid (f : term) : Prop := forall env, truth (sem f env).

Notation "a ||- b" := (valid (FImp a b)) (at level 61) : model_scope.
Notation "||- b" := (valid b) (at level 61) : model_scope.
Notation "a ⟛ b" := (valid (FImp a b) /\ valid (FImp b a)) (at level 61) : model_scope.
Open Scope valid_scope.
Open Scope model_scope.

Lemma valid_assumption : forall f, f ||- f.
Proof.
  by move=> f env /= h.
Qed.

Lemma valid_top :
  forall f,
  f ||- FTop.
Proof.
  by move=> f env /=.
Qed.

Lemma valid_top_l1 :
  forall f,
  FTop ||- f ->
       ||- f.
Proof.
  move=> f h env.
  by apply (h env).
Qed.

Lemma valid_top_l2 :
  forall f,
       ||- f ->
  FTop ||- f.
Proof.
  move=> f h env /= _.
  by apply h.
Qed.

Lemma valid_contradiction :
  forall f,
  FBot ||- f.
Proof.
  by move=> f env /=.
Qed.

Lemma valid_consistent :
  ~ ||- FBot.
Proof.
  move=> h.
  specialize (h (fun _ => VNat 0)).
  simpl in h.
  done.
Qed.

Lemma valid_and_intro :
  forall f g h,
  f ||- g ->
  f ||- h ->
  f ||- g ++ h.
Proof.
  move=> f g h h1 h2 env /= hf.
  split; by [apply h1|apply h2].
Qed.

Lemma valid_and_elim :
  forall f g h,
  f ||- g ++ h ->
  f ||- g /\ f ||- h.
Proof.
  move=> f g h h1.
  split=> env /= hf.
  - by apply (h1 env hf).
  - by apply (h1 env hf).
Qed.

Lemma valid_and_intro_l :
  forall f g h,
  g ||- f \/ h ||- f ->
  g ++ h ||- f.
Proof.
  move=> f g h [h1|h1] env /= [hg hh]; by [apply h1|apply h1].
Qed.

Lemma valid_and_l_cycle :
  forall f1 f2 f3 g,
  f1 ++ f2 ++ f3 ||- g ->
  f3 ++ f1 ++ f2 ||- g.
Proof.
  move=> f1 f2 f3 g h env /= [h3 [h1 h2]].
  by apply h.
Qed.

Lemma valid_imp_intro :
  forall f g h,
  g ++ f ||- h ->
       f ||- (FImp g h).
Proof.
  move=> f g h h1 env /= hf hg.
  by apply h1.
Qed.

Lemma valid_imp_elim :
  forall f g h,
  g ++ f ++ FImp f g ||- h ->
       f ++ FImp f g ||- h.
Proof.
  move=> f g h h1 env /= [hf hfg].
  apply h1.
  split=>//.
  by apply hfg.
Qed.

Lemma valid_weak :
  forall f1 f2 g,
        f2 ||- g ->
  f1 ++ f2 ||- g.
Proof.
  move=> f1 f2 g h env /= [_ h2].
  by apply h.
Qed.

Lemma valid_contr :
  forall f g,
  f ++ f ||- g ->
       f ||- g.
Proof.
  move=> f g h env /= hf.
  by apply h.
Qed.

Lemma valid_cut :
  forall f g h,
  f ||- g ->
  g ||- h ->
  f ||- h.
Proof.
  move=> f g h h1 h2 env /= hf.
  by apply h2, h1.
Qed.

Lemma valid_all_mono :
  forall f g,
  f ||- g ->
  FAll f ||- FAll g.
Proof.
  move=> f g h env /= hf d.
  by apply h, hf.
Qed.

Lemma valid_all_and :
  forall f g,
  FAll (f ++ g) ⟛ FAll f ++ FAll g.
Proof.
  move=> f g.
  split=> env /=.
  - move=> h.
    split=> d.
    + by apply (h d).
    + by apply (h d).
  - move=> [h1 h2] d.
    split.
    + by apply h1.
    + by apply h2.
Qed.

Lemma valid_all_de_bruijn :
  forall f g,
  f.[ren (+1)] ||- g ->
             f ||- FAll g.
Proof.
  move=> f g h env /= hf d.
  specialize (h (d .: env)).
  simpl in h.
  rewrite sem_ren in h.
  apply h.
  by have->: (+1) >>> (d .: env) = env by f_ext.
Qed.

Lemma valid_all_elim :
  forall f t,
  FAll f ||- f.[t/].
Proof.
  move=> f t env /= h.
  rewrite sem_subst.
  have->: (fun x => sem ((t .: ids) x) env) = sem t env .: env by f_ext=> -[|x].
  by apply h.
Qed.

End Model.